Loogle!

Result

Found 1006 declarations whose name contains "bind". Of these, 31 have a name containing "bind" and "measure".

• MeasureTheory.SimpleFunc.bind 📋 Mathlib.MeasureTheory.Function.SimpleFunc
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] (f : MeasureTheory.SimpleFunc α β) (g : β → MeasureTheory.SimpleFunc α γ) : MeasureTheory.SimpleFunc α γ
• MeasureTheory.SimpleFunc.bind_const 📋 Mathlib.MeasureTheory.Function.SimpleFunc
  {α : Type u_1} {β : Type u_2} [MeasurableSpace α] (f : MeasureTheory.SimpleFunc α β) : f.bind (MeasureTheory.SimpleFunc.const α) = f
• MeasureTheory.SimpleFunc.measurable_bind 📋 Mathlib.MeasureTheory.Function.SimpleFunc
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] [MeasurableSpace γ] (f : MeasureTheory.SimpleFunc α β) (g : β → α → γ) (hg : ∀ (b : β), Measurable (g b)) : Measurable fun a => g (f a) a
• MeasureTheory.SimpleFunc.bind_apply 📋 Mathlib.MeasureTheory.Function.SimpleFunc
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] (f : MeasureTheory.SimpleFunc α β) (g : β → MeasureTheory.SimpleFunc α γ) (a : α) : (f.bind g) a = (g (f a)) a
• MeasureTheory.Measure.bind 📋 Mathlib.MeasureTheory.Measure.GiryMonad
  {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (m : MeasureTheory.Measure α) (f : α → MeasureTheory.Measure β) : MeasureTheory.Measure β
• MeasureTheory.Measure.bind_dirac 📋 Mathlib.MeasureTheory.Measure.GiryMonad
  {α : Type u_1} {mα : MeasurableSpace α} {m : MeasureTheory.Measure α} : m.bind MeasureTheory.Measure.dirac = m
• MeasureTheory.Measure.join_eq_bind 📋 Mathlib.MeasureTheory.Measure.GiryMonad
  {α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure (MeasureTheory.Measure α)) : μ.join = μ.bind id
• MeasureTheory.Measure.dirac_bind 📋 Mathlib.MeasureTheory.Measure.GiryMonad
  {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α → MeasureTheory.Measure β} (hf : Measurable f) (a : α) : (MeasureTheory.Measure.dirac a).bind f = f a
• MeasureTheory.Measure.bind.eq_1 📋 Mathlib.MeasureTheory.Measure.GiryMonad
  {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (m : MeasureTheory.Measure α) (f : α → MeasureTheory.Measure β) : m.bind f = (MeasureTheory.Measure.map f m).join
• MeasureTheory.Measure.bind_dirac_eq_map 📋 Mathlib.MeasureTheory.Measure.GiryMonad
  {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (m : MeasureTheory.Measure α) {f : α → β} (hf : Measurable f) : (m.bind fun x => MeasureTheory.Measure.dirac (f x)) = MeasureTheory.Measure.map f m
• MeasureTheory.Measure.measurable_bind' 📋 Mathlib.MeasureTheory.Measure.GiryMonad
  {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {g : α → MeasureTheory.Measure β} (hg : Measurable g) : Measurable fun m => m.bind g
• MeasureTheory.Measure.bind_zero_left 📋 Mathlib.MeasureTheory.Measure.GiryMonad
  {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (f : α → MeasureTheory.Measure β) : MeasureTheory.Measure.bind 0 f = 0
• MeasureTheory.Measure.bind_zero_right' 📋 Mathlib.MeasureTheory.Measure.GiryMonad
  {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (m : MeasureTheory.Measure α) : (m.bind fun x => 0) = 0
• MeasureTheory.Measure.lintegral_bind_le 📋 Mathlib.MeasureTheory.Measure.GiryMonad
  {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (f : β → ENNReal) (m : MeasureTheory.Measure α) (μ : α → MeasureTheory.Measure β) : ∫⁻ (x : β), f x ∂m.bind μ ≤ ∫⁻ (a : α), ∫⁻ (x : β), f x ∂μ a ∂m
• MeasureTheory.Measure.bind_zero_right 📋 Mathlib.MeasureTheory.Measure.GiryMonad
  {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (m : MeasureTheory.Measure α) : m.bind 0 = 0
• MeasureTheory.Measure.bind_congr_right 📋 Mathlib.MeasureTheory.Measure.GiryMonad
  {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {f g : α → MeasureTheory.Measure β} (h : f =ᵐ[μ] g) : μ.bind f = μ.bind g
• MeasureTheory.Measure.aemeasurable_bind 📋 Mathlib.MeasureTheory.Measure.GiryMonad
  {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {g : α → MeasureTheory.Measure β} {m : MeasureTheory.Measure (MeasureTheory.Measure α)} (hg : AEMeasurable g m.join) : AEMeasurable (fun x => x.bind g) m
• MeasureTheory.Measure.bind_apply_le 📋 Mathlib.MeasureTheory.Measure.GiryMonad
  {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {m : MeasureTheory.Measure α} (f : α → MeasureTheory.Measure β) {s : Set β} (hs : MeasurableSet s) : (m.bind f) s ≤ ∫⁻ (a : α), (f a) s ∂m
• MeasureTheory.Measure.lintegral_bind 📋 Mathlib.MeasureTheory.Measure.GiryMonad
  {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {m : MeasureTheory.Measure α} {μ : α → MeasureTheory.Measure β} {f : β → ENNReal} (hμ : AEMeasurable μ m) (hf : AEMeasurable f (m.bind μ)) : ∫⁻ (x : β), f x ∂m.bind μ = ∫⁻ (a : α), ∫⁻ (x : β), f x ∂μ a ∂m
• MeasureTheory.Measure.bind_apply 📋 Mathlib.MeasureTheory.Measure.GiryMonad
  {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {m : MeasureTheory.Measure α} {f : α → MeasureTheory.Measure β} {s : Set β} (hs : MeasurableSet s) (hf : AEMeasurable f m) : (m.bind f) s = ∫⁻ (a : α), (f a) s ∂m
• MeasureTheory.Measure.bind_const 📋 Mathlib.MeasureTheory.Measure.GiryMonad
  {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {m : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} : (m.bind fun x => ν) = m Set.univ • ν
• MeasureTheory.Measure.bind_bind 📋 Mathlib.MeasureTheory.Measure.GiryMonad
  {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} [MeasurableSpace γ] {m : MeasureTheory.Measure α} {f : α → MeasureTheory.Measure β} {g : β → MeasureTheory.Measure γ} (hf : AEMeasurable f m) (hg : AEMeasurable g (m.bind f)) : (m.bind f).bind g = m.bind fun a => (f a).bind g
• MeasureTheory.Measure.ae_ae_of_ae_bind 📋 Mathlib.MeasureTheory.Measure.GiryMonad
  {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {m : MeasureTheory.Measure α} {f : α → MeasureTheory.Measure β} {p : β → Prop} (hf : AEMeasurable f m) (h : ∀ᵐ (b : β) ∂m.bind f, p b) : ∀ᵐ (a : α) ∂m, ∀ᵐ (b : β) ∂f a, p b
• MeasureTheory.Measure.instIsFiniteMeasureBindCoeKernelOfIsFiniteKernel 📋 Mathlib.Probability.Kernel.Composition.MeasureComp
  {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {κ : ProbabilityTheory.Kernel α β} [MeasureTheory.IsFiniteMeasure μ] [ProbabilityTheory.IsFiniteKernel κ] : MeasureTheory.IsFiniteMeasure (μ.bind ⇑κ)
• MeasureTheory.Measure.instIsProbabilityMeasureBindCoeKernelOfIsMarkovKernel 📋 Mathlib.Probability.Kernel.Composition.MeasureComp
  {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {κ : ProbabilityTheory.Kernel α β} [MeasureTheory.IsProbabilityMeasure μ] [ProbabilityTheory.IsMarkovKernel κ] : MeasureTheory.IsProbabilityMeasure (μ.bind ⇑κ)
• MeasureTheory.Measure.instIsZeroOrProbabilityMeasureBindCoeKernelOfIsZeroOrMarkovKernel 📋 Mathlib.Probability.Kernel.Composition.MeasureComp
  {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {κ : ProbabilityTheory.Kernel α β} [MeasureTheory.IsZeroOrProbabilityMeasure μ] [ProbabilityTheory.IsZeroOrMarkovKernel κ] : MeasureTheory.IsZeroOrProbabilityMeasure (μ.bind ⇑κ)
• MeasureTheory.Measure.instSFiniteBindCoeKernelOfIsSFiniteKernel 📋 Mathlib.Probability.Kernel.Composition.MeasureComp
  {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {κ : ProbabilityTheory.Kernel α β} [MeasureTheory.SFinite μ] [ProbabilityTheory.IsSFiniteKernel κ] : MeasureTheory.SFinite (μ.bind ⇑κ)
• PMF.toOuterMeasure_bind_apply 📋 Mathlib.Probability.ProbabilityMassFunction.Monad
  {α : Type u_1} {β : Type u_2} (p : PMF α) (f : α → PMF β) (s : Set β) : (p.bind f).toOuterMeasure s = ∑' (a : α), p a * (f a).toOuterMeasure s
• PMF.toMeasure_bind_apply 📋 Mathlib.Probability.ProbabilityMassFunction.Monad
  {α : Type u_1} {β : Type u_2} (p : PMF α) (f : α → PMF β) (s : Set β) [MeasurableSpace β] (hs : MeasurableSet s) : (p.bind f).toMeasure s = ∑' (a : α), p a * (f a).toMeasure s
• PMF.toOuterMeasure_bindOnSupport_apply 📋 Mathlib.Probability.ProbabilityMassFunction.Monad
  {α : Type u_1} {β : Type u_2} {p : PMF α} (f : (a : α) → a ∈ p.support → PMF β) (s : Set β) : (p.bindOnSupport f).toOuterMeasure s = ∑' (a : α), p a * if h : p a = 0 then 0 else (f a h).toOuterMeasure s
• PMF.toMeasure_bindOnSupport_apply 📋 Mathlib.Probability.ProbabilityMassFunction.Monad
  {α : Type u_1} {β : Type u_2} {p : PMF α} (f : (a : α) → a ∈ p.support → PMF β) (s : Set β) [MeasurableSpace β] (hs : MeasurableSet s) : (p.bindOnSupport f).toMeasure s = ∑' (a : α), p a * if h : p a = 0 then 0 else (f a h).toMeasure s

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using (by default) Ctrl-K Ctrl-S. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO.

This is Loogle revision 6ff4759 serving mathlib revision abad10c