Lean4
/-- * `𝔼 i ∈ s, f i` is notation for `Finset.expect s f`. It is the expectation of `f i` where `i`
ranges over the finite set `s` (either a `Finset` or a `Set` with a `Fintype` instance).
* `𝔼 i, f i` is notation for `Finset.expect Finset.univ f`. It is the expectation of `f i` where `i`
ranges over the finite domain of `f`.
* `𝔼 i ∈ s with p i, f i` is notation for `Finset.expect (Finset.filter p s) f`.
* `𝔼 (i ∈ s) (j ∈ t), f i j` is notation for `Finset.expect (s ×ˢ t) (fun ⟨i, j⟩ ↦ f i j)`.
These support destructuring, for example `𝔼 ⟨i, j⟩ ∈ s ×ˢ t, f i j`.
Notation: `"𝔼" bigOpBinders* ("with" term)? "," term` -/
@[scoped term_parser 1000]
public meta def bigexpect : Lean.ParserDescr✝ :=
ParserDescr.node✝ `BigOperators.bigexpect 1022
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "𝔼 ") BigOperators.bigOpBinders)
(ParserDescr.unary✝ `optional
(ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "with ") (ParserDescr.cat✝ `term 0))))
(ParserDescr.symbol✝ ", "))
(ParserDescr.cat✝ `term 67))
