Loogle!

Result

Found 79 definitions mentioning AEMeasurable and MeasureTheory.Measure.map.

• MeasureTheory.Measure.map_of_not_aemeasurable 📋 Mathlib.MeasureTheory.Measure.MeasureSpace
  {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α → β} {μ : MeasureTheory.Measure α} (hf : ¬AEMeasurable f μ) : MeasureTheory.Measure.map f μ = 0
• MeasureTheory.Measure.tendsto_ae_map 📋 Mathlib.MeasureTheory.Measure.MeasureSpace
  {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {f : α → β} (hf : AEMeasurable f μ) : Filter.Tendsto f (MeasureTheory.ae μ) (MeasureTheory.ae (MeasureTheory.Measure.map f μ))
• MeasureTheory.Measure.map_eq_zero_iff 📋 Mathlib.MeasureTheory.Measure.MeasureSpace
  {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {f : α → β} (hf : AEMeasurable f μ) : MeasureTheory.Measure.map f μ = 0 ↔ μ = 0
• MeasureTheory.Measure.map_ne_zero_iff 📋 Mathlib.MeasureTheory.Measure.MeasureSpace
  {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {f : α → β} (hf : AEMeasurable f μ) : MeasureTheory.Measure.map f μ ≠ 0 ↔ μ ≠ 0
• MeasureTheory.ae_of_ae_map 📋 Mathlib.MeasureTheory.Measure.MeasureSpace
  {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {f : α → β} (hf : AEMeasurable f μ) {p : β → Prop} (h : ∀ᵐ (y : β) ∂MeasureTheory.Measure.map f μ, p y) : ∀ᵐ (x : α) ∂μ, p (f x)
• MeasureTheory.Measure.map_apply_of_aemeasurable 📋 Mathlib.MeasureTheory.Measure.MeasureSpace
  {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {f : α → β} (hf : AEMeasurable f μ) {s : Set β} (hs : MeasurableSet s) : (MeasureTheory.Measure.map f μ) s = μ (f ⁻¹' s)
• MeasureTheory.ae_map_iff 📋 Mathlib.MeasureTheory.Measure.MeasureSpace
  {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {f : α → β} (hf : AEMeasurable f μ) {p : β → Prop} (hp : MeasurableSet {x | p x}) : (∀ᵐ (y : β) ∂MeasureTheory.Measure.map f μ, p y) ↔ ∀ᵐ (x : α) ∂μ, p (f x)
• MeasureTheory.mem_ae_of_mem_ae_map 📋 Mathlib.MeasureTheory.Measure.MeasureSpace
  {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {f : α → β} (hf : AEMeasurable f μ) {s : Set β} (hs : s ∈ MeasureTheory.ae (MeasureTheory.Measure.map f μ)) : f ⁻¹' s ∈ MeasureTheory.ae μ
• MeasureTheory.Measure.map_apply₀ 📋 Mathlib.MeasureTheory.Measure.MeasureSpace
  {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {f : α → β} (hf : AEMeasurable f μ) {s : Set β} (hs : MeasureTheory.NullMeasurableSet s (MeasureTheory.Measure.map f μ)) : (MeasureTheory.Measure.map f μ) s = μ (f ⁻¹' s)
• MeasureTheory.Measure.le_map_apply 📋 Mathlib.MeasureTheory.Measure.MeasureSpace
  {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {f : α → β} (hf : AEMeasurable f μ) (s : Set β) : μ (f ⁻¹' s) ≤ (MeasureTheory.Measure.map f μ) s
• MeasureTheory.Measure.le_map_apply_image 📋 Mathlib.MeasureTheory.Measure.MeasureSpace
  {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {f : α → β} (hf : AEMeasurable f μ) (s : Set α) : μ s ≤ (MeasureTheory.Measure.map f μ) (f '' s)
• MeasureTheory.Measure.preimage_null_of_map_null 📋 Mathlib.MeasureTheory.Measure.MeasureSpace
  {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {f : α → β} (hf : AEMeasurable f μ) {s : Set β} (hs : (MeasureTheory.Measure.map f μ) s = 0) : μ (f ⁻¹' s) = 0
• MeasureTheory.mem_ae_map_iff 📋 Mathlib.MeasureTheory.Measure.MeasureSpace
  {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {f : α → β} (hf : AEMeasurable f μ) {s : Set β} (hs : MeasurableSet s) : s ∈ MeasureTheory.ae (MeasureTheory.Measure.map f μ) ↔ f ⁻¹' s ∈ MeasureTheory.ae μ
• MeasureTheory.Measure.map_def 📋 Mathlib.MeasureTheory.Measure.MeasureSpace
  {α : Type u_8} {β : Type u_9} [MeasurableSpace α] [MeasurableSpace β] (f : α → β) (μ : MeasureTheory.Measure α) : MeasureTheory.Measure.map f μ = if hf : AEMeasurable f μ then (MeasureTheory.Measure.mapₗ (AEMeasurable.mk f hf)) μ else 0
• MeasureTheory.Measure.map_toOuterMeasure 📋 Mathlib.MeasureTheory.Measure.MeasureSpace
  {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {f : α → β} (hf : AEMeasurable f μ) : (MeasureTheory.Measure.map f μ).toOuterMeasure = ((MeasureTheory.OuterMeasure.map f) μ.toOuterMeasure).trim
• MeasureTheory.Measure.mapₗ_mk_apply_of_aemeasurable 📋 Mathlib.MeasureTheory.Measure.MeasureSpace
  {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {f : α → β} (hf : AEMeasurable f μ) : (MeasureTheory.Measure.mapₗ (AEMeasurable.mk f hf)) μ = MeasureTheory.Measure.map f μ
• MeasureTheory.ae_eq_comp 📋 Mathlib.MeasureTheory.Measure.Restrict
  {α : Type u_2} {β : Type u_3} {δ : Type u_4} {m0 : MeasurableSpace α} [MeasurableSpace β] {μ : MeasureTheory.Measure α} {f : α → β} {g g' : β → δ} (hf : AEMeasurable f μ) (h : g =ᵐ[MeasureTheory.Measure.map f μ] g') : g ∘ f =ᵐ[μ] g' ∘ f
• MeasureTheory.ae_eq_comp' 📋 Mathlib.MeasureTheory.Measure.Restrict
  {α : Type u_2} {β : Type u_3} {δ : Type u_4} {m0 : MeasurableSpace α} [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} {f : α → β} {g g' : β → δ} (hf : AEMeasurable f μ) (h : g =ᵐ[ν] g') (h2 : (MeasureTheory.Measure.map f μ).AbsolutelyContinuous ν) : g ∘ f =ᵐ[μ] g' ∘ f
• MeasureTheory.isProbabilityMeasure_map 📋 Mathlib.MeasureTheory.Measure.Typeclasses
  {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [MeasurableSpace β] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] {f : α → β} (hf : AEMeasurable f μ) : MeasureTheory.IsProbabilityMeasure (MeasureTheory.Measure.map f μ)
• MeasureTheory.SigmaFinite.of_map 📋 Mathlib.MeasureTheory.Measure.Typeclasses
  {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [MeasurableSpace β] (μ : MeasureTheory.Measure α) {f : α → β} (hf : AEMeasurable f μ) (h : MeasureTheory.SigmaFinite (MeasureTheory.Measure.map f μ)) : MeasureTheory.SigmaFinite μ
• aemeasurable_of_map_neZero 📋 Mathlib.MeasureTheory.Measure.AEMeasurable
  {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [MeasurableSpace β] {μ : MeasureTheory.Measure α} {f : α → β} (h : NeZero (MeasureTheory.Measure.map f μ)) : AEMeasurable f μ
• AEMeasurable.comp_aemeasurable' 📋 Mathlib.MeasureTheory.Measure.AEMeasurable
  {α : Type u_2} {β : Type u_3} {δ : Type u_5} {m0 : MeasurableSpace α} [MeasurableSpace β] [MeasurableSpace δ] {μ : MeasureTheory.Measure α} {f : α → δ} {g : δ → β} (hg : AEMeasurable g (MeasureTheory.Measure.map f μ)) (hf : AEMeasurable f μ) : AEMeasurable (fun x => g (f x)) μ
• AEMeasurable.comp_measurable 📋 Mathlib.MeasureTheory.Measure.AEMeasurable
  {α : Type u_2} {β : Type u_3} {δ : Type u_5} {m0 : MeasurableSpace α} [MeasurableSpace β] [MeasurableSpace δ] {μ : MeasureTheory.Measure α} {f : α → δ} {g : δ → β} (hg : AEMeasurable g (MeasureTheory.Measure.map f μ)) (hf : Measurable f) : AEMeasurable (g ∘ f) μ
• AEMeasurable.comp_aemeasurable 📋 Mathlib.MeasureTheory.Measure.AEMeasurable
  {α : Type u_2} {β : Type u_3} {δ : Type u_5} {m0 : MeasurableSpace α} [MeasurableSpace β] [MeasurableSpace δ] {μ : MeasureTheory.Measure α} {f : α → δ} {g : δ → β} (hg : AEMeasurable g (MeasureTheory.Measure.map f μ)) (hf : AEMeasurable f μ) : AEMeasurable (g ∘ f) μ
• MeasurableEmbedding.aemeasurable_map_iff 📋 Mathlib.MeasureTheory.Measure.AEMeasurable
  {α : Type u_2} {β : Type u_3} {γ : Type u_4} {m0 : MeasurableSpace α} [MeasurableSpace β] [MeasurableSpace γ] {f : α → β} {μ : MeasureTheory.Measure α} {g : β → γ} (hf : MeasurableEmbedding f) : AEMeasurable g (MeasureTheory.Measure.map f μ) ↔ AEMeasurable (g ∘ f) μ
• MeasureTheory.Measure.map_sum 📋 Mathlib.MeasureTheory.Measure.AEMeasurable
  {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [MeasurableSpace β] {ι : Type u_7} {m : ι → MeasureTheory.Measure α} {f : α → β} (hf : AEMeasurable f (MeasureTheory.Measure.sum m)) : MeasureTheory.Measure.map f (MeasureTheory.Measure.sum m) = MeasureTheory.Measure.sum fun i => MeasureTheory.Measure.map f (m i)
• MeasureTheory.Measure.restrict_map_of_aemeasurable 📋 Mathlib.MeasureTheory.Measure.AEMeasurable
  {α : Type u_2} {δ : Type u_5} {m0 : MeasurableSpace α} [MeasurableSpace δ] {μ : MeasureTheory.Measure α} {f : α → δ} (hf : AEMeasurable f μ) {s : Set δ} (hs : MeasurableSet s) : (MeasureTheory.Measure.map f μ).restrict s = MeasureTheory.Measure.map f (μ.restrict (f ⁻¹' s))
• AEMeasurable.map_map_of_aemeasurable 📋 Mathlib.MeasureTheory.Measure.AEMeasurable
  {α : Type u_2} {β : Type u_3} {γ : Type u_4} {m0 : MeasurableSpace α} [MeasurableSpace β] [MeasurableSpace γ] {μ : MeasureTheory.Measure α} {g : β → γ} {f : α → β} (hg : AEMeasurable g (MeasureTheory.Measure.map f μ)) (hf : AEMeasurable f μ) : MeasureTheory.Measure.map g (MeasureTheory.Measure.map f μ) = MeasureTheory.Measure.map (g ∘ f) μ
• MeasureTheory.Measure.map_mono_of_aemeasurable 📋 Mathlib.MeasureTheory.Measure.AEMeasurable
  {α : Type u_2} {δ : Type u_5} {m0 : MeasurableSpace α} [MeasurableSpace δ] {μ ν : MeasureTheory.Measure α} {f : α → δ} (h : μ ≤ ν) (hf : AEMeasurable f ν) : MeasureTheory.Measure.map f μ ≤ MeasureTheory.Measure.map f ν
• aemeasurable_map_equiv_iff 📋 Mathlib.MeasureTheory.Measure.AEMeasurable
  {α : Type u_2} {β : Type u_3} {γ : Type u_4} {m0 : MeasurableSpace α} [MeasurableSpace β] [MeasurableSpace γ] {μ : MeasureTheory.Measure α} (e : α ≃ᵐ β) {f : β → γ} : AEMeasurable f (MeasureTheory.Measure.map (⇑e) μ) ↔ AEMeasurable (f ∘ ⇑e) μ
• MeasureTheory.Measure.InnerRegularWRT.map 📋 Mathlib.MeasureTheory.Measure.Regular
  {α : Type u_2} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {pa qa : Set α → Prop} (H : μ.InnerRegularWRT pa qa) {f : α → β} (hf : AEMeasurable f μ) {pb qb : Set β → Prop} (hAB : ∀ (U : Set β), qb U → qa (f ⁻¹' U)) (hAB' : ∀ (K : Set α), pa K → pb (f '' K)) (hB₂ : ∀ (U : Set β), qb U → MeasurableSet U) : (MeasureTheory.Measure.map f μ).InnerRegularWRT pb qb
• essSup_comp_le_essSup_map_measure 📋 Mathlib.MeasureTheory.Function.EssSup
  {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [CompleteLattice β] {γ : Type u_3} {mγ : MeasurableSpace γ} {f : α → γ} {g : γ → β} (hf : AEMeasurable f μ) : essSup (g ∘ f) μ ≤ essSup g (MeasureTheory.Measure.map f μ)
• essSup_map_measure_of_measurable 📋 Mathlib.MeasureTheory.Function.EssSup
  {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [CompleteLattice β] {γ : Type u_3} {mγ : MeasurableSpace γ} {f : α → γ} {g : γ → β} [MeasurableSpace β] [TopologicalSpace β] [SecondCountableTopology β] [OrderClosedTopology β] [OpensMeasurableSpace β] (hg : Measurable g) (hf : AEMeasurable f μ) : essSup g (MeasureTheory.Measure.map f μ) = essSup (g ∘ f) μ
• essSup_map_measure 📋 Mathlib.MeasureTheory.Function.EssSup
  {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [CompleteLattice β] {γ : Type u_3} {mγ : MeasurableSpace γ} {f : α → γ} {g : γ → β} [MeasurableSpace β] [TopologicalSpace β] [SecondCountableTopology β] [OrderClosedTopology β] [OpensMeasurableSpace β] (hg : AEMeasurable g (MeasureTheory.Measure.map f μ)) (hf : AEMeasurable f μ) : essSup g (MeasureTheory.Measure.map f μ) = essSup (g ∘ f) μ
• MeasureTheory.lintegral_map' 📋 Mathlib.MeasureTheory.Integral.Lebesgue
  {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {mβ : MeasurableSpace β} {f : β → ENNReal} {g : α → β} (hf : AEMeasurable f (MeasureTheory.Measure.map g μ)) (hg : AEMeasurable g μ) : ∫⁻ (a : β), f a ∂MeasureTheory.Measure.map g μ = ∫⁻ (a : α), f (g a) ∂μ
• MeasureTheory.AEStronglyMeasurable.comp_aemeasurable 📋 Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
  {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {g : α → β} {γ : Type u_5} {x✝ : MeasurableSpace γ} {x✝¹ : MeasurableSpace α} {f : γ → α} {μ : MeasureTheory.Measure γ} (hg : MeasureTheory.AEStronglyMeasurable g (MeasureTheory.Measure.map f μ)) (hf : AEMeasurable f μ) : MeasureTheory.AEStronglyMeasurable (g ∘ f) μ
• MeasureTheory.Memℒp.comp_of_map 📋 Mathlib.MeasureTheory.Function.LpSeminorm.Basic
  {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {β : Type u_5} {mβ : MeasurableSpace β} {f : α → β} {g : β → E} (hg : MeasureTheory.Memℒp g p (MeasureTheory.Measure.map f μ)) (hf : AEMeasurable f μ) : MeasureTheory.Memℒp (g ∘ f) p μ
• MeasureTheory.eLpNormEssSup_map_measure 📋 Mathlib.MeasureTheory.Function.LpSeminorm.Basic
  {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {β : Type u_5} {mβ : MeasurableSpace β} {f : α → β} {g : β → E} (hg : MeasureTheory.AEStronglyMeasurable g (MeasureTheory.Measure.map f μ)) (hf : AEMeasurable f μ) : MeasureTheory.eLpNormEssSup g (MeasureTheory.Measure.map f μ) = MeasureTheory.eLpNormEssSup (g ∘ f) μ
• MeasureTheory.snormEssSup_map_measure 📋 Mathlib.MeasureTheory.Function.LpSeminorm.Basic
  {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {β : Type u_5} {mβ : MeasurableSpace β} {f : α → β} {g : β → E} (hg : MeasureTheory.AEStronglyMeasurable g (MeasureTheory.Measure.map f μ)) (hf : AEMeasurable f μ) : MeasureTheory.eLpNormEssSup g (MeasureTheory.Measure.map f μ) = MeasureTheory.eLpNormEssSup (g ∘ f) μ
• MeasureTheory.memℒp_map_measure_iff 📋 Mathlib.MeasureTheory.Function.LpSeminorm.Basic
  {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {β : Type u_5} {mβ : MeasurableSpace β} {f : α → β} {g : β → E} (hg : MeasureTheory.AEStronglyMeasurable g (MeasureTheory.Measure.map f μ)) (hf : AEMeasurable f μ) : MeasureTheory.Memℒp g p (MeasureTheory.Measure.map f μ) ↔ MeasureTheory.Memℒp (g ∘ f) p μ
• MeasureTheory.eLpNorm_map_measure 📋 Mathlib.MeasureTheory.Function.LpSeminorm.Basic
  {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {β : Type u_5} {mβ : MeasurableSpace β} {f : α → β} {g : β → E} (hg : MeasureTheory.AEStronglyMeasurable g (MeasureTheory.Measure.map f μ)) (hf : AEMeasurable f μ) : MeasureTheory.eLpNorm g p (MeasureTheory.Measure.map f μ) = MeasureTheory.eLpNorm (g ∘ f) p μ
• MeasureTheory.snorm_map_measure 📋 Mathlib.MeasureTheory.Function.LpSeminorm.Basic
  {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {β : Type u_5} {mβ : MeasurableSpace β} {f : α → β} {g : β → E} (hg : MeasureTheory.AEStronglyMeasurable g (MeasureTheory.Measure.map f μ)) (hf : AEMeasurable f μ) : MeasureTheory.eLpNorm g p (MeasureTheory.Measure.map f μ) = MeasureTheory.eLpNorm (g ∘ f) p μ
• MeasureTheory.Integrable.comp_aemeasurable 📋 Mathlib.MeasureTheory.Function.L1Space
  {α : Type u_1} {β : Type u_2} {δ : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasurableSpace δ] [NormedAddCommGroup β] {f : α → δ} {g : δ → β} (hg : MeasureTheory.Integrable g (MeasureTheory.Measure.map f μ)) (hf : AEMeasurable f μ) : MeasureTheory.Integrable (g ∘ f) μ
• MeasureTheory.integrable_map_measure 📋 Mathlib.MeasureTheory.Function.L1Space
  {α : Type u_1} {β : Type u_2} {δ : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasurableSpace δ] [NormedAddCommGroup β] {f : α → δ} {g : δ → β} (hg : MeasureTheory.AEStronglyMeasurable g (MeasureTheory.Measure.map f μ)) (hf : AEMeasurable f μ) : MeasureTheory.Integrable g (MeasureTheory.Measure.map f μ) ↔ MeasureTheory.Integrable (g ∘ f) μ
• MeasureTheory.integral_map 📋 Mathlib.MeasureTheory.Integral.Bochner
  {α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] [NormedSpace ℝ G] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_7} [MeasurableSpace β] {φ : α → β} (hφ : AEMeasurable φ μ) {f : β → G} (hfm : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.map φ μ)) : ∫ (y : β), f y ∂MeasureTheory.Measure.map φ μ = ∫ (x : α), f (φ x) ∂μ
• MeasureTheory.setIntegral_map 📋 Mathlib.MeasureTheory.Integral.SetIntegral
  {X : Type u_1} {E : Type u_3} [MeasurableSpace X] [NormedAddCommGroup E] [NormedSpace ℝ E] {μ : MeasureTheory.Measure X} {Y : Type u_5} [MeasurableSpace Y] {g : X → Y} {f : Y → E} {s : Set Y} (hs : MeasurableSet s) (hf : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.map g μ)) (hg : AEMeasurable g μ) : ∫ (y : Y) in s, f y ∂MeasureTheory.Measure.map g μ = ∫ (x : X) in g ⁻¹' s, f (g x) ∂μ
• MeasureTheory.set_integral_map 📋 Mathlib.MeasureTheory.Integral.SetIntegral
  {X : Type u_1} {E : Type u_3} [MeasurableSpace X] [NormedAddCommGroup E] [NormedSpace ℝ E] {μ : MeasureTheory.Measure X} {Y : Type u_5} [MeasurableSpace Y] {g : X → Y} {f : Y → E} {s : Set Y} (hs : MeasurableSet s) (hf : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.map g μ)) (hg : AEMeasurable g μ) : ∫ (y : Y) in s, f y ∂MeasureTheory.Measure.map g μ = ∫ (x : X) in g ⁻¹' s, f (g x) ∂μ
• MeasureTheory.Measure.fst_map_prod_mk₀ 📋 Mathlib.MeasureTheory.Measure.Prod
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] {X : α → β} {Y : α → γ} {μ : MeasureTheory.Measure α} (hY : AEMeasurable Y μ) : (MeasureTheory.Measure.map (fun a => (X a, Y a)) μ).fst = MeasureTheory.Measure.map X μ
• MeasureTheory.Measure.snd_map_prod_mk₀ 📋 Mathlib.MeasureTheory.Measure.Prod
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] {X : α → β} {Y : α → γ} {μ : MeasureTheory.Measure α} (hX : AEMeasurable X μ) : (MeasureTheory.Measure.map (fun a => (X a, Y a)) μ).snd = MeasureTheory.Measure.map Y μ
• essSup_comp_quotientAddGroup_mk 📋 Mathlib.MeasureTheory.Measure.Haar.Quotient
  {G : Type u_1} [AddGroup G] [MeasurableSpace G] [TopologicalSpace G] [TopologicalAddGroup G] [BorelSpace G] {μ : MeasureTheory.Measure G} {Γ : AddSubgroup G} {𝓕 : Set G} (h𝓕 : MeasureTheory.IsAddFundamentalDomain (↥Γ.op) 𝓕 μ) [Countable ↥Γ] [MeasurableSpace (G ⧸ Γ)] [BorelSpace (G ⧸ Γ)] [μ.IsAddRightInvariant] {g : G ⧸ Γ → ENNReal} (g_ae_measurable : AEMeasurable g (MeasureTheory.Measure.map QuotientAddGroup.mk (μ.restrict 𝓕))) : essSup g (MeasureTheory.Measure.map QuotientAddGroup.mk (μ.restrict 𝓕)) = essSup (fun x => g ↑x) μ
• essSup_comp_quotientGroup_mk 📋 Mathlib.MeasureTheory.Measure.Haar.Quotient
  {G : Type u_1} [Group G] [MeasurableSpace G] [TopologicalSpace G] [TopologicalGroup G] [BorelSpace G] {μ : MeasureTheory.Measure G} {Γ : Subgroup G} {𝓕 : Set G} (h𝓕 : MeasureTheory.IsFundamentalDomain (↥Γ.op) 𝓕 μ) [Countable ↥Γ] [MeasurableSpace (G ⧸ Γ)] [BorelSpace (G ⧸ Γ)] [μ.IsMulRightInvariant] {g : G ⧸ Γ → ENNReal} (g_ae_measurable : AEMeasurable g (MeasureTheory.Measure.map QuotientGroup.mk (μ.restrict 𝓕))) : essSup g (MeasureTheory.Measure.map QuotientGroup.mk (μ.restrict 𝓕)) = essSup (fun x => g ↑x) μ
• MeasureTheory.AEStronglyMeasurable.comp_ae_measurable' 📋 Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace β] {mα : MeasurableSpace α} {x✝ : MeasurableSpace γ} {f : α → β} {μ : MeasureTheory.Measure γ} {g : γ → α} (hf : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.map g μ)) (hg : AEMeasurable g μ) : MeasureTheory.AEStronglyMeasurable' (MeasurableSpace.comap g mα) (f ∘ g) μ
• MeasureTheory.ProbabilityMeasure.toMeasure_map 📋 Mathlib.MeasureTheory.Measure.ProbabilityMeasure
  {Ω : Type u_1} {Ω' : Type u_2} [MeasurableSpace Ω] [MeasurableSpace Ω'] (ν : MeasureTheory.ProbabilityMeasure Ω) {f : Ω → Ω'} (hf : AEMeasurable f ↑ν) : ↑(ν.map hf) = MeasureTheory.Measure.map f ↑ν
• MeasureTheory.ProbabilityMeasure.map.eq_1 📋 Mathlib.MeasureTheory.Measure.ProbabilityMeasure
  {Ω : Type u_1} {Ω' : Type u_2} [MeasurableSpace Ω] [MeasurableSpace Ω'] (ν : MeasureTheory.ProbabilityMeasure Ω) {f : Ω → Ω'} (f_aemble : AEMeasurable f ↑ν) : ν.map f_aemble = ⟨MeasureTheory.Measure.map f ↑ν, ⋯⟩
• ProbabilityTheory.indepFun_iff_map_prod_eq_prod_map_map 📋 Mathlib.Probability.Independence.Basic
  {Ω : Type u_1} {β : Type u_6} {β' : Type u_7} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {f : Ω → β} {g : Ω → β'} {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'} [MeasureTheory.IsFiniteMeasure μ] (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) : ProbabilityTheory.IndepFun f g μ ↔ MeasureTheory.Measure.map (fun ω => (f ω, g ω)) μ = (MeasureTheory.Measure.map f μ).prod (MeasureTheory.Measure.map g μ)
• Real.hasPDF_iff_of_aemeasurable 📋 Mathlib.Probability.Density
  {Ω : Type u_1} {m : MeasurableSpace Ω} {ℙ : MeasureTheory.Measure Ω} {X : Ω → ℝ} [MeasureTheory.SFinite ℙ] (hX : AEMeasurable X ℙ) : MeasureTheory.HasPDF X ℙ MeasureTheory.volume ↔ (MeasureTheory.Measure.map X ℙ).AbsolutelyContinuous MeasureTheory.volume
• Real.hasPDF_iff 📋 Mathlib.Probability.Density
  {Ω : Type u_1} {m : MeasurableSpace Ω} {ℙ : MeasureTheory.Measure Ω} {X : Ω → ℝ} [MeasureTheory.SFinite ℙ] : MeasureTheory.HasPDF X ℙ MeasureTheory.volume ↔ AEMeasurable X ℙ ∧ (MeasureTheory.Measure.map X ℙ).AbsolutelyContinuous MeasureTheory.volume
• MeasureTheory.hasPDF_iff_of_aemeasurable 📋 Mathlib.Probability.Density
  {Ω : Type u_1} {E : Type u_2} [MeasurableSpace E] {x✝ : MeasurableSpace Ω} {X : Ω → E} {ℙ : MeasureTheory.Measure Ω} {μ : MeasureTheory.Measure E} (hX : AEMeasurable X ℙ) : MeasureTheory.HasPDF X ℙ μ ↔ (MeasureTheory.Measure.map X ℙ).HaveLebesgueDecomposition μ ∧ (MeasureTheory.Measure.map X ℙ).AbsolutelyContinuous μ
• MeasureTheory.HasPDF.mk 📋 Mathlib.Probability.Density
  {Ω : Type u_1} {E : Type u_2} [MeasurableSpace E] {m : MeasurableSpace Ω} {X : Ω → E} {ℙ : MeasureTheory.Measure Ω} {μ : autoParam (MeasureTheory.Measure E) _auto✝} (aemeasurable' : AEMeasurable X ℙ) (haveLebesgueDecomposition' : (MeasureTheory.Measure.map X ℙ).HaveLebesgueDecomposition μ) (absolutelyContinuous' : (MeasureTheory.Measure.map X ℙ).AbsolutelyContinuous μ) : MeasureTheory.HasPDF X ℙ μ
• MeasureTheory.hasPDF_iff 📋 Mathlib.Probability.Density
  {Ω : Type u_1} {E : Type u_2} [MeasurableSpace E] {x✝ : MeasurableSpace Ω} {X : Ω → E} {ℙ : MeasureTheory.Measure Ω} {μ : MeasureTheory.Measure E} : MeasureTheory.HasPDF X ℙ μ ↔ AEMeasurable X ℙ ∧ (MeasureTheory.Measure.map X ℙ).HaveLebesgueDecomposition μ ∧ (MeasureTheory.Measure.map X ℙ).AbsolutelyContinuous μ
• MeasureTheory.hasPDF_of_map_eq_withDensity 📋 Mathlib.Probability.Density
  {Ω : Type u_1} {E : Type u_2} [MeasurableSpace E] {x✝ : MeasurableSpace Ω} {X : Ω → E} {ℙ : MeasureTheory.Measure Ω} {μ : MeasureTheory.Measure E} (hX : AEMeasurable X ℙ) (f : E → ENNReal) (hf : AEMeasurable f μ) (h : MeasureTheory.Measure.map X ℙ = μ.withDensity f) : MeasureTheory.HasPDF X ℙ μ
• MeasureTheory.pdf.eq_of_map_eq_withDensity 📋 Mathlib.Probability.Density
  {Ω : Type u_1} {E : Type u_2} [MeasurableSpace E] {m : MeasurableSpace Ω} {ℙ : MeasureTheory.Measure Ω} {μ : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasure ℙ] {X : Ω → E} [MeasureTheory.HasPDF X ℙ μ] (f : E → ENNReal) (hmf : AEMeasurable f μ) : MeasureTheory.Measure.map X ℙ = μ.withDensity f ↔ MeasureTheory.pdf X ℙ μ =ᵐ[μ] f
• MeasureTheory.pdf.eq_of_map_eq_withDensity' 📋 Mathlib.Probability.Density
  {Ω : Type u_1} {E : Type u_2} [MeasurableSpace E] {m : MeasurableSpace Ω} {ℙ : MeasureTheory.Measure Ω} {μ : MeasureTheory.Measure E} [MeasureTheory.SigmaFinite μ] {X : Ω → E} [MeasureTheory.HasPDF X ℙ μ] (f : E → ENNReal) (hmf : AEMeasurable f μ) : MeasureTheory.Measure.map X ℙ = μ.withDensity f ↔ MeasureTheory.pdf X ℙ μ =ᵐ[μ] f
• ProbabilityTheory.IdentDistrib.mk 📋 Mathlib.Probability.IdentDistrib
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] {f : α → γ} {g : β → γ} {μ : autoParam (MeasureTheory.Measure α) _auto✝} {ν : autoParam (MeasureTheory.Measure β) _auto✝¹} (aemeasurable_fst : AEMeasurable f μ) (aemeasurable_snd : AEMeasurable g ν) (map_eq : MeasureTheory.Measure.map f μ = MeasureTheory.Measure.map g ν) : ProbabilityTheory.IdentDistrib f g μ ν
• ProbabilityTheory.IdentDistrib.comp_of_aemeasurable 📋 Mathlib.Probability.IdentDistrib
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] [MeasurableSpace δ] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} {f : α → γ} {g : β → γ} {u : γ → δ} (h : ProbabilityTheory.IdentDistrib f g μ ν) (hu : AEMeasurable u (MeasureTheory.Measure.map f μ)) : ProbabilityTheory.IdentDistrib (u ∘ f) (u ∘ g) μ ν
• MeasureTheory.Integrable.condDistrib_ae_map 📋 Mathlib.Probability.Kernel.CondDistrib
  {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] [NormedAddCommGroup F] {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {X : α → β} {Y : α → Ω} {mβ : MeasurableSpace β} {f : β × Ω → F} (hY : AEMeasurable Y μ) (hf_int : MeasureTheory.Integrable f (MeasureTheory.Measure.map (fun a => (X a, Y a)) μ)) : ∀ᵐ (b : β) ∂MeasureTheory.Measure.map X μ, MeasureTheory.Integrable (fun ω => f (b, ω)) ((ProbabilityTheory.condDistrib Y X μ) b)
• MeasureTheory.Integrable.integral_condDistrib_map 📋 Mathlib.Probability.Kernel.CondDistrib
  {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] [NormedAddCommGroup F] {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {X : α → β} {Y : α → Ω} {mβ : MeasurableSpace β} {f : β × Ω → F} [NormedSpace ℝ F] (hY : AEMeasurable Y μ) (hf_int : MeasureTheory.Integrable f (MeasureTheory.Measure.map (fun a => (X a, Y a)) μ)) : MeasureTheory.Integrable (fun x => ∫ (y : Ω), f (x, y) ∂(ProbabilityTheory.condDistrib Y X μ) x) (MeasureTheory.Measure.map X μ)
• MeasureTheory.Integrable.condDistrib_ae 📋 Mathlib.Probability.Kernel.CondDistrib
  {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] [NormedAddCommGroup F] {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {X : α → β} {Y : α → Ω} {mβ : MeasurableSpace β} {f : β × Ω → F} (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ) (hf_int : MeasureTheory.Integrable f (MeasureTheory.Measure.map (fun a => (X a, Y a)) μ)) : ∀ᵐ (a : α) ∂μ, MeasureTheory.Integrable (fun ω => f (X a, ω)) ((ProbabilityTheory.condDistrib Y X μ) (X a))
• MeasureTheory.Integrable.integral_condDistrib 📋 Mathlib.Probability.Kernel.CondDistrib
  {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] [NormedAddCommGroup F] {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {X : α → β} {Y : α → Ω} {mβ : MeasurableSpace β} {f : β × Ω → F} [NormedSpace ℝ F] (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ) (hf_int : MeasureTheory.Integrable f (MeasureTheory.Measure.map (fun a => (X a, Y a)) μ)) : MeasureTheory.Integrable (fun a => ∫ (y : Ω), f (X a, y) ∂(ProbabilityTheory.condDistrib Y X μ) (X a)) μ
• MeasureTheory.Integrable.norm_integral_condDistrib_map 📋 Mathlib.Probability.Kernel.CondDistrib
  {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] [NormedAddCommGroup F] {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {X : α → β} {Y : α → Ω} {mβ : MeasurableSpace β} {f : β × Ω → F} [NormedSpace ℝ F] (hY : AEMeasurable Y μ) (hf_int : MeasureTheory.Integrable f (MeasureTheory.Measure.map (fun a => (X a, Y a)) μ)) : MeasureTheory.Integrable (fun x => ‖∫ (y : Ω), f (x, y) ∂(ProbabilityTheory.condDistrib Y X μ) x‖) (MeasureTheory.Measure.map X μ)
• MeasureTheory.Integrable.integral_norm_condDistrib_map 📋 Mathlib.Probability.Kernel.CondDistrib
  {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] [NormedAddCommGroup F] {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {X : α → β} {Y : α → Ω} {mβ : MeasurableSpace β} {f : β × Ω → F} (hY : AEMeasurable Y μ) (hf_int : MeasureTheory.Integrable f (MeasureTheory.Measure.map (fun a => (X a, Y a)) μ)) : MeasureTheory.Integrable (fun x => ∫ (y : Ω), ‖f (x, y)‖ ∂(ProbabilityTheory.condDistrib Y X μ) x) (MeasureTheory.Measure.map X μ)
• MeasureTheory.Integrable.norm_integral_condDistrib 📋 Mathlib.Probability.Kernel.CondDistrib
  {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] [NormedAddCommGroup F] {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {X : α → β} {Y : α → Ω} {mβ : MeasurableSpace β} {f : β × Ω → F} [NormedSpace ℝ F] (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ) (hf_int : MeasureTheory.Integrable f (MeasureTheory.Measure.map (fun a => (X a, Y a)) μ)) : MeasureTheory.Integrable (fun a => ‖∫ (y : Ω), f (X a, y) ∂(ProbabilityTheory.condDistrib Y X μ) (X a)‖) μ
• MeasureTheory.Integrable.integral_norm_condDistrib 📋 Mathlib.Probability.Kernel.CondDistrib
  {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] [NormedAddCommGroup F] {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {X : α → β} {Y : α → Ω} {mβ : MeasurableSpace β} {f : β × Ω → F} (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ) (hf_int : MeasureTheory.Integrable f (MeasureTheory.Measure.map (fun a => (X a, Y a)) μ)) : MeasureTheory.Integrable (fun a => ∫ (y : Ω), ‖f (X a, y)‖ ∂(ProbabilityTheory.condDistrib Y X μ) (X a)) μ
• MeasureTheory.AEStronglyMeasurable.integral_condDistrib_map 📋 Mathlib.Probability.Kernel.CondDistrib
  {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] [NormedAddCommGroup F] {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {X : α → β} {Y : α → Ω} {mβ : MeasurableSpace β} {f : β × Ω → F} [NormedSpace ℝ F] (hY : AEMeasurable Y μ) (hf : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.map (fun a => (X a, Y a)) μ)) : MeasureTheory.AEStronglyMeasurable (fun x => ∫ (y : Ω), f (x, y) ∂(ProbabilityTheory.condDistrib Y X μ) x) (MeasureTheory.Measure.map X μ)
• MeasureTheory.AEStronglyMeasurable.integral_condDistrib 📋 Mathlib.Probability.Kernel.CondDistrib
  {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] [NormedAddCommGroup F] {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {X : α → β} {Y : α → Ω} {mβ : MeasurableSpace β} {f : β × Ω → F} [NormedSpace ℝ F] (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ) (hf : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.map (fun a => (X a, Y a)) μ)) : MeasureTheory.AEStronglyMeasurable (fun a => ∫ (y : Ω), f (X a, y) ∂(ProbabilityTheory.condDistrib Y X μ) (X a)) μ
• ProbabilityTheory.aestronglyMeasurable'_integral_condDistrib 📋 Mathlib.Probability.Kernel.CondDistrib
  {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] [NormedAddCommGroup F] {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {X : α → β} {Y : α → Ω} {mβ : MeasurableSpace β} {f : β × Ω → F} [NormedSpace ℝ F] (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ) (hf : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.map (fun a => (X a, Y a)) μ)) : MeasureTheory.AEStronglyMeasurable' (MeasurableSpace.comap X mβ) (fun a => ∫ (y : Ω), f (X a, y) ∂(ProbabilityTheory.condDistrib Y X μ) (X a)) μ
• ProbabilityTheory.condexp_prod_ae_eq_integral_condDistrib' 📋 Mathlib.Probability.Kernel.CondDistrib
  {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] [NormedAddCommGroup F] {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {X : α → β} {Y : α → Ω} {mβ : MeasurableSpace β} {f : β × Ω → F} [NormedSpace ℝ F] [CompleteSpace F] (hX : Measurable X) (hY : AEMeasurable Y μ) (hf_int : MeasureTheory.Integrable f (MeasureTheory.Measure.map (fun a => (X a, Y a)) μ)) : (MeasureTheory.condexp (MeasurableSpace.comap X mβ) μ fun a => f (X a, Y a)) =ᵐ[μ] fun a => ∫ (y : Ω), f (X a, y) ∂(ProbabilityTheory.condDistrib Y X μ) (X a)
• ProbabilityTheory.condexp_prod_ae_eq_integral_condDistrib₀ 📋 Mathlib.Probability.Kernel.CondDistrib
  {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] [NormedAddCommGroup F] {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {X : α → β} {Y : α → Ω} {mβ : MeasurableSpace β} {f : β × Ω → F} [NormedSpace ℝ F] [CompleteSpace F] (hX : Measurable X) (hY : AEMeasurable Y μ) (hf : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.map (fun a => (X a, Y a)) μ)) (hf_int : MeasureTheory.Integrable (fun a => f (X a, Y a)) μ) : (MeasureTheory.condexp (MeasurableSpace.comap X mβ) μ fun a => f (X a, Y a)) =ᵐ[μ] fun a => ∫ (y : Ω), f (X a, y) ∂(ProbabilityTheory.condDistrib Y X μ) (X a)
• MeasureTheory.AEStronglyMeasurable.ae_integrable_condDistrib_map_iff 📋 Mathlib.Probability.Kernel.CondDistrib
  {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] [NormedAddCommGroup F] {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {X : α → β} {Y : α → Ω} {mβ : MeasurableSpace β} {f : β × Ω → F} (hY : AEMeasurable Y μ) (hf : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.map (fun a => (X a, Y a)) μ)) : (∀ᵐ (a : β) ∂MeasureTheory.Measure.map X μ, MeasureTheory.Integrable (fun ω => f (a, ω)) ((ProbabilityTheory.condDistrib Y X μ) a)) ∧ MeasureTheory.Integrable (fun a => ∫ (ω : Ω), ‖f (a, ω)‖ ∂(ProbabilityTheory.condDistrib Y X μ) a) (MeasureTheory.Measure.map X μ) ↔ MeasureTheory.Integrable f (MeasureTheory.Measure.map (fun a => (X a, Y a)) μ)

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, _ * _, _ ^ _, |- _ < _ → _
woould 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 4e1aab0 serving mathlib revision b513113