Loogle!
Result
Found 430 declarations mentioning MeasureTheory.Measure.map. Of these, only the first 200 are shown.
- MeasureTheory.Measure.map 📋 Mathlib.MeasureTheory.Measure.Map
{α : Type u_4} {β : Type u_5} [MeasurableSpace α] [MeasurableSpace β] (f : α → β) (μ : MeasureTheory.Measure α) : MeasureTheory.Measure β - MeasureTheory.Measure.map_id 📋 Mathlib.MeasureTheory.Measure.Map
{α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} : MeasureTheory.Measure.map id μ = μ - MeasureTheory.Measure.map_id' 📋 Mathlib.MeasureTheory.Measure.Map
{α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} : MeasureTheory.Measure.map (fun x => x) μ = μ - AEMeasurable.of_map_ne_zero 📋 Mathlib.MeasureTheory.Measure.Map
{α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α → β} {μ : MeasureTheory.Measure α} (hf : MeasureTheory.Measure.map f μ ≠ 0) : AEMeasurable f μ - MeasureTheory.Measure.map_of_not_aemeasurable 📋 Mathlib.MeasureTheory.Measure.Map
{α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α → β} {μ : MeasureTheory.Measure α} (hf : ¬AEMeasurable f μ) : MeasureTheory.Measure.map f μ = 0 - MeasureTheory.Measure.map_zero 📋 Mathlib.MeasureTheory.Measure.Map
{α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (f : α → β) : MeasureTheory.Measure.map f 0 = 0 - MeasurableEquiv.map_measurableEquiv_injective 📋 Mathlib.MeasureTheory.Measure.Map
{α : Type u_1} {β : Type u_2} {x✝ : MeasurableSpace α} [MeasurableSpace β] (e : α ≃ᵐ β) : Function.Injective (MeasureTheory.Measure.map ⇑e) - MeasureTheory.Measure.map_congr 📋 Mathlib.MeasureTheory.Measure.Map
{α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {f g : α → β} (h : f =ᵐ[μ] g) : MeasureTheory.Measure.map f μ = MeasureTheory.Measure.map g μ - MeasureTheory.ae_map_mem_range 📋 Mathlib.MeasureTheory.Measure.Map
{α : Type u_1} {β : Type u_2} {mβ : MeasurableSpace β} {m0 : MeasurableSpace α} (f : α → β) (hf : MeasurableSet (Set.range f)) (μ : MeasureTheory.Measure α) : ∀ᵐ (x : β) ∂MeasureTheory.Measure.map f μ, x ∈ Set.range f - MeasureTheory.Measure.tendsto_ae_map 📋 Mathlib.MeasureTheory.Measure.Map
{α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {f : α → β} (hf : AEMeasurable f μ) : Filter.Tendsto f (MeasureTheory.ae μ) (MeasureTheory.ae (MeasureTheory.Measure.map f μ)) - MeasureTheory.Measure.map_map 📋 Mathlib.MeasureTheory.Measure.Map
{α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {μ : MeasureTheory.Measure α} {g : β → γ} {f : α → β} (hg : Measurable g) (hf : Measurable f) : MeasureTheory.Measure.map g (MeasureTheory.Measure.map f μ) = MeasureTheory.Measure.map (g ∘ f) μ - MeasurableEmbedding.map_apply 📋 Mathlib.MeasureTheory.Measure.Map
{α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} {m1 : MeasurableSpace β} {f : α → β} (hf : MeasurableEmbedding f) (μ : MeasureTheory.Measure α) (s : Set β) : (MeasureTheory.Measure.map f μ) s = μ (f ⁻¹' s) - MeasureTheory.Measure.map_eq_zero_iff 📋 Mathlib.MeasureTheory.Measure.Map
{α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {f : α → β} (hf : AEMeasurable f μ) : MeasureTheory.Measure.map f μ = 0 ↔ μ = 0 - MeasureTheory.Measure.map_ne_zero_iff 📋 Mathlib.MeasureTheory.Measure.Map
{α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {f : α → β} (hf : AEMeasurable f μ) : MeasureTheory.Measure.map f μ ≠ 0 ↔ μ ≠ 0 - MeasureTheory.ae_of_ae_map 📋 Mathlib.MeasureTheory.Measure.Map
{α : Type u_1} {β : Type u_2} {mα : 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.measure_preimage_of_map_eq_self 📋 Mathlib.MeasureTheory.Measure.Map
{α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → α} (hf : MeasureTheory.Measure.map f μ = μ) {s : Set α} (hs : MeasureTheory.NullMeasurableSet s μ) : μ (f ⁻¹' s) = μ s - MeasureTheory.Measure.map_apply 📋 Mathlib.MeasureTheory.Measure.Map
{α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {f : α → β} (hf : Measurable f) {s : Set β} (hs : MeasurableSet s) : (MeasureTheory.Measure.map f μ) s = μ (f ⁻¹' s) - MeasureTheory.Measure.map_apply_of_aemeasurable 📋 Mathlib.MeasureTheory.Measure.Map
{α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {f : α → β} (hf : AEMeasurable f μ) {s : Set β} (hs : MeasurableSet s) : (MeasureTheory.Measure.map f μ) s = μ (f ⁻¹' s) - MeasureTheory.Measure.le_map_apply 📋 Mathlib.MeasureTheory.Measure.Map
{α : Type u_1} {β : Type u_2} {mα : 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.Map
{α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {f : α → β} (hf : AEMeasurable f μ) (s : Set α) : μ s ≤ (MeasureTheory.Measure.map f μ) (f '' s) - MeasureTheory.Measure.map_mono 📋 Mathlib.MeasureTheory.Measure.Map
{α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ ν : MeasureTheory.Measure α} {f : α → β} (h : μ ≤ ν) (hf : Measurable f) : MeasureTheory.Measure.map f μ ≤ MeasureTheory.Measure.map f ν - MeasureTheory.ae_map_iff 📋 Mathlib.MeasureTheory.Measure.Map
{α : Type u_1} {β : Type u_2} {mα : 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.Map
{α : Type u_1} {β : Type u_2} {mα : 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.Map
{α : Type u_1} {β : Type u_2} {mα : 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.preimage_null_of_map_null 📋 Mathlib.MeasureTheory.Measure.Map
{α : Type u_1} {β : Type u_2} {mα : 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.Map
{α : Type u_1} {β : Type u_2} {mα : 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_add 📋 Mathlib.MeasureTheory.Measure.Map
{α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (μ ν : MeasureTheory.Measure α) {f : α → β} (hf : Measurable f) : MeasureTheory.Measure.map f (μ + ν) = MeasureTheory.Measure.map f μ + MeasureTheory.Measure.map f ν - MeasurableEquiv.map_map_symm 📋 Mathlib.MeasureTheory.Measure.Map
{α : Type u_1} {β : Type u_2} {x✝ : MeasurableSpace α} [MeasurableSpace β] {ν : MeasureTheory.Measure β} (e : α ≃ᵐ β) : MeasureTheory.Measure.map (⇑e) (MeasureTheory.Measure.map (⇑e.symm) ν) = ν - MeasurableEquiv.map_symm_map 📋 Mathlib.MeasureTheory.Measure.Map
{α : Type u_1} {β : Type u_2} {x✝ : MeasurableSpace α} [MeasurableSpace β] {μ : MeasureTheory.Measure α} (e : α ≃ᵐ β) : MeasureTheory.Measure.map (⇑e.symm) (MeasureTheory.Measure.map (⇑e) μ) = μ - MeasureTheory.Measure.map_smul 📋 Mathlib.MeasureTheory.Measure.Map
{α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {R : Type u_4} [SMul R ENNReal] [IsScalarTower R ENNReal ENNReal] (c : R) (μ : MeasureTheory.Measure α) (f : α → β) : MeasureTheory.Measure.map f (c • μ) = c • MeasureTheory.Measure.map f μ - MeasurableEquiv.map_apply_eq_iff_map_symm_apply_eq 📋 Mathlib.MeasureTheory.Measure.Map
{α : Type u_1} {β : Type u_2} {x✝ : MeasurableSpace α} [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} (e : α ≃ᵐ β) : MeasureTheory.Measure.map (⇑e) μ = ν ↔ μ = MeasureTheory.Measure.map (⇑e.symm) ν - MeasurableEquiv.map_ae 📋 Mathlib.MeasureTheory.Measure.Map
{α : Type u_1} {β : Type u_2} {x✝ : MeasurableSpace α} [MeasurableSpace β] (f : α ≃ᵐ β) (μ : MeasureTheory.Measure α) : Filter.map (⇑f) (MeasureTheory.ae μ) = MeasureTheory.ae (MeasureTheory.Measure.map (⇑f) μ) - MeasurableEquiv.map_apply 📋 Mathlib.MeasureTheory.Measure.Map
{α : Type u_1} {β : Type u_2} {x✝ : MeasurableSpace α} [MeasurableSpace β] {μ : MeasureTheory.Measure α} (f : α ≃ᵐ β) (s : Set β) : (MeasureTheory.Measure.map (⇑f) μ) s = μ (⇑f ⁻¹' s) - MeasureTheory.Measure.map_toOuterMeasure 📋 Mathlib.MeasureTheory.Measure.Map
{α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {f : α → β} (hf : AEMeasurable f μ) : (MeasureTheory.Measure.map f μ).toOuterMeasure = ((MeasureTheory.OuterMeasure.map f) μ.toOuterMeasure).trim - MeasureTheory.Measure.mapₗ_apply_of_measurable 📋 Mathlib.MeasureTheory.Measure.Map
{α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α → β} (hf : Measurable f) (μ : MeasureTheory.Measure α) : (MeasureTheory.Measure.mapₗ f) μ = MeasureTheory.Measure.map f μ - MeasureTheory.Measure.mapₗ_mk_apply_of_aemeasurable 📋 Mathlib.MeasureTheory.Measure.Map
{α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {f : α → β} (hf : AEMeasurable f μ) : (MeasureTheory.Measure.mapₗ (AEMeasurable.mk f hf)) μ = MeasureTheory.Measure.map f μ - MeasureTheory.Measure.map_def 📋 Mathlib.MeasureTheory.Measure.Map
{α : Type u_4} {β : Type u_5} [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_smul_nnreal 📋 Mathlib.MeasureTheory.Measure.Map
{α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (c : NNReal) (μ : MeasureTheory.Measure α) (f : α → β) : MeasureTheory.Measure.map f (c • μ) = c • MeasureTheory.Measure.map f μ - MeasureTheory.Measure.comap_swap 📋 Mathlib.MeasureTheory.Measure.Comap
{α : Type u_1} {β : Type u_2} {ma : MeasurableSpace α} {mb : MeasurableSpace β} (μ : MeasureTheory.Measure (α × β)) : MeasureTheory.Measure.comap Prod.swap μ = MeasureTheory.Measure.map Prod.swap μ - MeasurableEquiv.comap_symm 📋 Mathlib.MeasureTheory.Measure.Comap
{α : Type u_1} {β : Type u_2} {ma : MeasurableSpace α} {mb : MeasurableSpace β} {μ : MeasureTheory.Measure α} (e : α ≃ᵐ β) : MeasureTheory.Measure.comap (⇑e.symm) μ = MeasureTheory.Measure.map (⇑e) μ - MeasurableEquiv.map_symm 📋 Mathlib.MeasureTheory.Measure.Comap
{α : Type u_1} {β : Type u_2} {ma : MeasurableSpace α} {mb : MeasurableSpace β} {μ : MeasureTheory.Measure α} (e : β ≃ᵐ α) : MeasureTheory.Measure.map (⇑e.symm) μ = MeasureTheory.Measure.comap (⇑e) μ - MeasurableEmbedding.absolutelyContinuous_map 📋 Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
{α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} {m1 : MeasurableSpace β} {f : α → β} {μ ν : MeasureTheory.Measure α} (hf : MeasurableEmbedding f) (hμν : μ.AbsolutelyContinuous ν) : (MeasureTheory.Measure.map f μ).AbsolutelyContinuous (MeasureTheory.Measure.map f ν) - MeasureTheory.Measure.AbsolutelyContinuous.map 📋 Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
{α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ ν : MeasureTheory.Measure α} (h : μ.AbsolutelyContinuous ν) {f : α → β} (hf : Measurable f) : (MeasureTheory.Measure.map f μ).AbsolutelyContinuous (MeasureTheory.Measure.map f ν) - Measurable.quasiMeasurePreserving 📋 Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
{α : Type u_1} {β : Type u_2} {mβ : MeasurableSpace β} {f : α → β} {_m0 : MeasurableSpace α} (hf : Measurable f) (μ : MeasureTheory.Measure α) : MeasureTheory.Measure.QuasiMeasurePreserving f μ (MeasureTheory.Measure.map f μ) - MeasureTheory.Measure.QuasiMeasurePreserving.absolutelyContinuous 📋 Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
{α : Type u_1} {β : Type u_2} {mβ : MeasurableSpace β} {m0 : MeasurableSpace α} {f : α → β} {μa : autoParam (MeasureTheory.Measure α) _auto✝} {μb : autoParam (MeasureTheory.Measure β) _auto✝¹} (self : MeasureTheory.Measure.QuasiMeasurePreserving f μa μb) : (MeasureTheory.Measure.map f μa).AbsolutelyContinuous μb - MeasureTheory.Measure.QuasiMeasurePreserving.mk 📋 Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
{α : Type u_1} {β : Type u_2} {mβ : MeasurableSpace β} {m0 : MeasurableSpace α} {f : α → β} {μa : autoParam (MeasureTheory.Measure α) _auto✝} {μb : autoParam (MeasureTheory.Measure β) _auto✝¹} (measurable : Measurable f) (absolutelyContinuous : (MeasureTheory.Measure.map f μa).AbsolutelyContinuous μb) : MeasureTheory.Measure.QuasiMeasurePreserving f μa μb - MeasureTheory.Measure.QuasiMeasurePreserving.ae_map_le 📋 Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
{α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μa : MeasureTheory.Measure α} {μb : MeasureTheory.Measure β} {f : α → β} (h : MeasureTheory.Measure.QuasiMeasurePreserving f μa μb) : MeasureTheory.ae (MeasureTheory.Measure.map f μa) ≤ MeasureTheory.ae μb - MeasurableEquiv.quasiMeasurePreserving_symm 📋 Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
{α : Type u_1} {β : Type u_2} {x✝ : MeasurableSpace α} [MeasurableSpace β] (μ : MeasureTheory.Measure α) (e : α ≃ᵐ β) : MeasureTheory.Measure.QuasiMeasurePreserving (⇑e.symm) (MeasureTheory.Measure.map (⇑e) μ) μ - MeasurableEmbedding.comap_map 📋 Mathlib.MeasureTheory.Measure.Restrict
{α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} {m1 : MeasurableSpace β} {f : α → β} (hf : MeasurableEmbedding f) (μ : MeasureTheory.Measure α) : MeasureTheory.Measure.comap f (MeasureTheory.Measure.map f μ) = μ - MeasurableEmbedding.map_comap 📋 Mathlib.MeasureTheory.Measure.Restrict
{α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} {m1 : MeasurableSpace β} {f : α → β} (hf : MeasurableEmbedding f) (μ : MeasureTheory.Measure β) : MeasureTheory.Measure.map f (MeasureTheory.Measure.comap f μ) = μ.restrict (Set.range f) - MeasurableEmbedding.restrict_map 📋 Mathlib.MeasureTheory.Measure.Restrict
{α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} {m1 : MeasurableSpace β} {f : α → β} (hf : MeasurableEmbedding f) (μ : MeasureTheory.Measure α) (s : Set β) : (MeasureTheory.Measure.map f μ).restrict s = MeasureTheory.Measure.map f (μ.restrict (f ⁻¹' s)) - MeasureTheory.Measure.restrict_map 📋 Mathlib.MeasureTheory.Measure.Restrict
{α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [MeasurableSpace β] {μ : MeasureTheory.Measure α} {f : α → β} (hf : Measurable f) {s : Set β} (hs : MeasurableSet s) : (MeasureTheory.Measure.map f μ).restrict s = MeasureTheory.Measure.map f (μ.restrict (f ⁻¹' s)) - MeasurableEmbedding.ae_map_iff 📋 Mathlib.MeasureTheory.Measure.Restrict
{α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} {m1 : MeasurableSpace β} {f : α → β} (hf : MeasurableEmbedding f) {p : β → Prop} {μ : MeasureTheory.Measure α} : (∀ᵐ (x : β) ∂MeasureTheory.Measure.map f μ, p x) ↔ ∀ᵐ (x : α) ∂μ, p (f x) - 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 - map_comap_subtype_coe 📋 Mathlib.MeasureTheory.Measure.Restrict
{α : Type u_2} {m0 : MeasurableSpace α} {s : Set α} (hs : MeasurableSet s) (μ : MeasureTheory.Measure α) : MeasureTheory.Measure.map Subtype.val (MeasureTheory.Measure.comap Subtype.val μ) = μ.restrict s - MeasurableSet.map_coe_volume 📋 Mathlib.MeasureTheory.Measure.Restrict
{α : Type u_2} [MeasureTheory.MeasureSpace α] {s : Set α} (hs : MeasurableSet s) : MeasureTheory.Measure.map Subtype.val MeasureTheory.volume = MeasureTheory.volume.restrict s - MeasurableEquiv.restrict_map 📋 Mathlib.MeasureTheory.Measure.Restrict
{α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} {m1 : MeasurableSpace β} (e : α ≃ᵐ β) (μ : MeasureTheory.Measure α) (s : Set β) : (MeasureTheory.Measure.map (⇑e) μ).restrict s = MeasureTheory.Measure.map (⇑e) (μ.restrict (⇑e ⁻¹' s)) - MeasureTheory.Measure.isFiniteMeasure_map 📋 Mathlib.MeasureTheory.Measure.Typeclasses.Finite
{α : Type u_1} {β : Type u_2} [MeasurableSpace β] {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] (f : α → β) : MeasureTheory.IsFiniteMeasure (MeasureTheory.Measure.map f μ) - MeasurableEmbedding.sigmaFinite_map 📋 Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
{α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [MeasurableSpace β] {μ : MeasureTheory.Measure α} {f : α → β} (hf : MeasurableEmbedding f) [MeasureTheory.SigmaFinite μ] : MeasureTheory.SigmaFinite (MeasureTheory.Measure.map f μ) - MeasureTheory.SigmaFinite.of_map 📋 Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
{α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [MeasurableSpace β] (μ : MeasureTheory.Measure α) {f : α → β} (hf : AEMeasurable f μ) (h : MeasureTheory.SigmaFinite (MeasureTheory.Measure.map f μ)) : MeasureTheory.SigmaFinite μ - MeasurableEquiv.sigmaFinite_map 📋 Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
{α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [MeasurableSpace β] {μ : MeasureTheory.Measure α} (f : α ≃ᵐ β) [MeasureTheory.SigmaFinite μ] : MeasureTheory.SigmaFinite (MeasureTheory.Measure.map (⇑f) μ) - MeasureTheory.trim_eq_map 📋 Mathlib.MeasureTheory.Measure.Trim
{α : Type u_1} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m ≤ m0) : μ.trim hm = MeasureTheory.Measure.map id μ - MeasureTheory.Measure.instSFiniteMap 📋 Mathlib.MeasureTheory.Measure.AEMeasurable
{α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [MeasurableSpace β] (μ : MeasureTheory.Measure α) (f : α → β) [MeasureTheory.SFinite μ] : MeasureTheory.SFinite (MeasureTheory.Measure.map f μ) - 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) μ - Measurable.measurePreserving 📋 Mathlib.Dynamics.Ergodic.MeasurePreserving
{α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {f : α → β} (h : Measurable f) (μa : MeasureTheory.Measure α) : MeasureTheory.MeasurePreserving f μa (MeasureTheory.Measure.map f μa) - MeasureTheory.MeasurePreserving.map_eq 📋 Mathlib.Dynamics.Ergodic.MeasurePreserving
{α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {f : α → β} {μa : autoParam (MeasureTheory.Measure α) _auto✝} {μb : autoParam (MeasureTheory.Measure β) _auto✝¹} (self : MeasureTheory.MeasurePreserving f μa μb) : MeasureTheory.Measure.map f μa = μb - MeasureTheory.MeasurePreserving.mk 📋 Mathlib.Dynamics.Ergodic.MeasurePreserving
{α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {f : α → β} {μa : autoParam (MeasureTheory.Measure α) _auto✝} {μb : autoParam (MeasureTheory.Measure β) _auto✝¹} (measurable : Measurable f) (map_eq : MeasureTheory.Measure.map f μa = μb) : MeasureTheory.MeasurePreserving f μa μb - MeasureTheory.MeasurableEquiv.measurePreserving_symm 📋 Mathlib.Dynamics.Ergodic.MeasurePreserving
{α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (μ : MeasureTheory.Measure α) (e : α ≃ᵐ β) : MeasureTheory.MeasurePreserving (⇑e.symm) (MeasureTheory.Measure.map (⇑e) μ) μ - IsFiniteMeasureOnCompacts.map 📋 Mathlib.MeasureTheory.Constructions.BorelSpace.Order
{α : Type u_1} {β : Type u_2} [TopologicalSpace α] {mα : MeasurableSpace α} [BorelSpace α] [TopologicalSpace β] {mβ : MeasurableSpace β} [BorelSpace β] (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasureOnCompacts μ] (f : α ≃ₜ β) : MeasureTheory.IsFiniteMeasureOnCompacts (MeasureTheory.Measure.map (⇑f) μ) - MeasureTheory.Measure.InnerRegular.map_of_continuous 📋 Mathlib.MeasureTheory.Measure.Regular
{α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace α] [BorelSpace α] [MeasurableSpace β] [TopologicalSpace β] [BorelSpace β] [h : μ.InnerRegular] {f : α → β} (hf : Continuous f) : (MeasureTheory.Measure.map f μ).InnerRegular - MeasureTheory.Measure.InnerRegularCompactLTTop.map_of_continuous 📋 Mathlib.MeasureTheory.Measure.Regular
{α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace α] [BorelSpace α] [MeasurableSpace β] [TopologicalSpace β] [BorelSpace β] [h : μ.InnerRegularCompactLTTop] {f : α → β} (hf : Continuous f) : (MeasureTheory.Measure.map f μ).InnerRegularCompactLTTop - MeasureTheory.Measure.InnerRegular.map 📋 Mathlib.MeasureTheory.Measure.Regular
{α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace α] [BorelSpace α] [MeasurableSpace β] [TopologicalSpace β] [BorelSpace β] [μ.InnerRegular] (f : α ≃ₜ β) : (MeasureTheory.Measure.map (⇑f) μ).InnerRegular - MeasureTheory.Measure.OuterRegular.map 📋 Mathlib.MeasureTheory.Measure.Regular
{α : Type u_1} {β : Type u_2} [MeasurableSpace α] [TopologicalSpace α] [OpensMeasurableSpace α] [MeasurableSpace β] [TopologicalSpace β] [BorelSpace β] (f : α ≃ₜ β) (μ : MeasureTheory.Measure α) [μ.OuterRegular] : (MeasureTheory.Measure.map (⇑f) μ).OuterRegular - MeasureTheory.Measure.Regular.map 📋 Mathlib.MeasureTheory.Measure.Regular
{α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace α] [BorelSpace α] [MeasurableSpace β] [TopologicalSpace β] [BorelSpace β] [μ.Regular] (f : α ≃ₜ β) : (MeasureTheory.Measure.map (⇑f) μ).Regular - MeasureTheory.Measure.InnerRegular.map_iff 📋 Mathlib.MeasureTheory.Measure.Regular
{α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace α] [BorelSpace α] [MeasurableSpace β] [TopologicalSpace β] [BorelSpace β] (f : α ≃ₜ β) : (MeasureTheory.Measure.map (⇑f) μ).InnerRegular ↔ μ.InnerRegular - MeasureTheory.Measure.Regular.map_iff 📋 Mathlib.MeasureTheory.Measure.Regular
{α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace α] [BorelSpace α] [MeasurableSpace β] [TopologicalSpace β] [BorelSpace β] (f : α ≃ₜ β) : (MeasureTheory.Measure.map (⇑f) μ).Regular ↔ μ.Regular - 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 - 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 : α ≃ᵐ β) {pb qb : Set β → Prop} (hAB : ∀ (U : Set β), qb U → qa (⇑f ⁻¹' U)) (hAB' : ∀ (K : Set α), pa K → pb (⇑f '' K)) : (MeasureTheory.Measure.map (⇑f) μ).InnerRegularWRT pb qb - MeasureTheory.Measure.IsAddLeftInvariant.map_add_left_eq_self 📋 Mathlib.MeasureTheory.Group.Defs
{G : Type u_1} {inst✝ : MeasurableSpace G} {inst✝¹ : Add G} {μ : MeasureTheory.Measure G} [self : μ.IsAddLeftInvariant] (g : G) : MeasureTheory.Measure.map (fun x => g + x) μ = μ - MeasureTheory.Measure.IsAddLeftInvariant.mk 📋 Mathlib.MeasureTheory.Group.Defs
{G : Type u_1} [MeasurableSpace G] [Add G] {μ : MeasureTheory.Measure G} (map_add_left_eq_self : ∀ (g : G), MeasureTheory.Measure.map (fun x => g + x) μ = μ) : μ.IsAddLeftInvariant - MeasureTheory.Measure.IsAddRightInvariant.map_add_right_eq_self 📋 Mathlib.MeasureTheory.Group.Defs
{G : Type u_1} {inst✝ : MeasurableSpace G} {inst✝¹ : Add G} {μ : MeasureTheory.Measure G} [self : μ.IsAddRightInvariant] (g : G) : MeasureTheory.Measure.map (fun x => x + g) μ = μ - MeasureTheory.Measure.IsAddRightInvariant.mk 📋 Mathlib.MeasureTheory.Group.Defs
{G : Type u_1} [MeasurableSpace G] [Add G] {μ : MeasureTheory.Measure G} (map_add_right_eq_self : ∀ (g : G), MeasureTheory.Measure.map (fun x => x + g) μ = μ) : μ.IsAddRightInvariant - MeasureTheory.Measure.IsMulLeftInvariant.map_mul_left_eq_self 📋 Mathlib.MeasureTheory.Group.Defs
{G : Type u_1} {inst✝ : MeasurableSpace G} {inst✝¹ : Mul G} {μ : MeasureTheory.Measure G} [self : μ.IsMulLeftInvariant] (g : G) : MeasureTheory.Measure.map (fun x => g * x) μ = μ - MeasureTheory.Measure.IsMulLeftInvariant.mk 📋 Mathlib.MeasureTheory.Group.Defs
{G : Type u_1} [MeasurableSpace G] [Mul G] {μ : MeasureTheory.Measure G} (map_mul_left_eq_self : ∀ (g : G), MeasureTheory.Measure.map (fun x => g * x) μ = μ) : μ.IsMulLeftInvariant - MeasureTheory.Measure.IsMulRightInvariant.map_mul_right_eq_self 📋 Mathlib.MeasureTheory.Group.Defs
{G : Type u_1} {inst✝ : MeasurableSpace G} {inst✝¹ : Mul G} {μ : MeasureTheory.Measure G} [self : μ.IsMulRightInvariant] (g : G) : MeasureTheory.Measure.map (fun x => x * g) μ = μ - MeasureTheory.Measure.IsMulRightInvariant.mk 📋 Mathlib.MeasureTheory.Group.Defs
{G : Type u_1} [MeasurableSpace G] [Mul G] {μ : MeasureTheory.Measure G} (map_mul_right_eq_self : ∀ (g : G), MeasureTheory.Measure.map (fun x => x * g) μ = μ) : μ.IsMulRightInvariant - MeasureTheory.map_smul 📋 Mathlib.MeasureTheory.Group.Action
{M : Type v} {α : Type w} {m : MeasurableSpace α} [MeasurableSpace M] [SMul M α] [MeasurableSMul M α] (c : M) (μ : MeasureTheory.Measure α) [MeasureTheory.SMulInvariantMeasure M α μ] : MeasureTheory.Measure.map (fun x => c • x) μ = μ - MeasureTheory.map_vadd 📋 Mathlib.MeasureTheory.Group.Action
{M : Type v} {α : Type w} {m : MeasurableSpace α} [MeasurableSpace M] [VAdd M α] [MeasurableVAdd M α] (c : M) (μ : MeasureTheory.Measure α) [MeasureTheory.VAddInvariantMeasure M α μ] : MeasureTheory.Measure.map (fun x => c +ᵥ x) μ = μ - MeasureTheory.smulInvariantMeasure_map_smul 📋 Mathlib.MeasureTheory.Group.Action
{M : Type uM} {N : Type uN} {α : Type uα} [MeasurableSpace M] [MeasurableSpace N] [MeasurableSpace α] [SMul M α] [SMul N α] [SMulCommClass N M α] [MeasurableSMul M α] [MeasurableSMul N α] (μ : MeasureTheory.Measure α) [MeasureTheory.SMulInvariantMeasure M α μ] (n : N) : MeasureTheory.SMulInvariantMeasure M α (MeasureTheory.Measure.map (fun x => n • x) μ) - MeasureTheory.vaddInvariantMeasure_map_vadd 📋 Mathlib.MeasureTheory.Group.Action
{M : Type uM} {N : Type uN} {α : Type uα} [MeasurableSpace M] [MeasurableSpace N] [MeasurableSpace α] [VAdd M α] [VAdd N α] [VAddCommClass N M α] [MeasurableVAdd M α] [MeasurableVAdd N α] (μ : MeasureTheory.Measure α) [MeasureTheory.VAddInvariantMeasure M α μ] (n : N) : MeasureTheory.VAddInvariantMeasure M α (MeasureTheory.Measure.map (fun x => n +ᵥ x) μ) - MeasureTheory.smulInvariantMeasure_map 📋 Mathlib.MeasureTheory.Group.Action
{M : Type uM} {α : Type uα} {β : Type uβ} [MeasurableSpace M] [MeasurableSpace α] [MeasurableSpace β] [SMul M α] [SMul M β] [MeasurableSMul M β] (μ : MeasureTheory.Measure α) [MeasureTheory.SMulInvariantMeasure M α μ] (f : α → β) (hsmul : ∀ (m : M) (a : α), f (m • a) = m • f a) (hf : Measurable f) : MeasureTheory.SMulInvariantMeasure M β (MeasureTheory.Measure.map f μ) - MeasureTheory.vaddInvariantMeasure_map 📋 Mathlib.MeasureTheory.Group.Action
{M : Type uM} {α : Type uα} {β : Type uβ} [MeasurableSpace M] [MeasurableSpace α] [MeasurableSpace β] [VAdd M α] [VAdd M β] [MeasurableVAdd M β] (μ : MeasureTheory.Measure α) [MeasureTheory.VAddInvariantMeasure M α μ] (f : α → β) (hsmul : ∀ (m : M) (a : α), f (m +ᵥ a) = m +ᵥ f a) (hf : Measurable f) : MeasureTheory.VAddInvariantMeasure M β (MeasureTheory.Measure.map f μ) - MeasureTheory.smulInvariantMeasure_tfae 📋 Mathlib.MeasureTheory.Group.Action
(G : Type u) {α : Type w} {m : MeasurableSpace α} [Group G] [MulAction G α] (μ : MeasureTheory.Measure α) [MeasurableSpace G] [MeasurableSMul G α] : [MeasureTheory.SMulInvariantMeasure G α μ, ∀ (c : G) (s : Set α), MeasurableSet s → μ ((fun x => c • x) ⁻¹' s) = μ s, ∀ (c : G) (s : Set α), MeasurableSet s → μ (c • s) = μ s, ∀ (c : G) (s : Set α), μ ((fun x => c • x) ⁻¹' s) = μ s, ∀ (c : G) (s : Set α), μ (c • s) = μ s, ∀ (c : G), MeasureTheory.Measure.map (fun x => c • x) μ = μ, ∀ (c : G), MeasureTheory.MeasurePreserving (fun x => c • x) μ μ].TFAE - MeasureTheory.vaddInvariantMeasure_tfae 📋 Mathlib.MeasureTheory.Group.Action
(G : Type u) {α : Type w} {m : MeasurableSpace α} [AddGroup G] [AddAction G α] (μ : MeasureTheory.Measure α) [MeasurableSpace G] [MeasurableVAdd G α] : [MeasureTheory.VAddInvariantMeasure G α μ, ∀ (c : G) (s : Set α), MeasurableSet s → μ ((fun x => c +ᵥ x) ⁻¹' s) = μ s, ∀ (c : G) (s : Set α), MeasurableSet s → μ (c +ᵥ s) = μ s, ∀ (c : G) (s : Set α), μ ((fun x => c +ᵥ x) ⁻¹' s) = μ s, ∀ (c : G) (s : Set α), μ (c +ᵥ s) = μ s, ∀ (c : G), MeasureTheory.Measure.map (fun x => c +ᵥ x) μ = μ, ∀ (c : G), MeasureTheory.MeasurePreserving (fun x => c +ᵥ x) μ μ].TFAE - MeasureTheory.SimpleFunc.lintegral_map 📋 Mathlib.MeasureTheory.Function.SimpleFunc
{α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_5} [MeasurableSpace β] (g : MeasureTheory.SimpleFunc β ENNReal) {f : α → β} (hf : Measurable f) : g.lintegral (MeasureTheory.Measure.map f μ) = (g.comp f hf).lintegral μ - MeasureTheory.lintegral_map_le 📋 Mathlib.MeasureTheory.Integral.Lebesgue.Map
{α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} (f : β → ENNReal) (g : α → β) : ∫⁻ (a : β), f a ∂MeasureTheory.Measure.map g μ ≤ ∫⁻ (a : α), f (g a) ∂μ - MeasurableEmbedding.lintegral_map 📋 Mathlib.MeasureTheory.Integral.Lebesgue.Map
{α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {g : α → β} (hg : MeasurableEmbedding g) (f : β → ENNReal) : ∫⁻ (a : β), f a ∂MeasureTheory.Measure.map g μ = ∫⁻ (a : α), f (g a) ∂μ - MeasureTheory.lintegral_map 📋 Mathlib.MeasureTheory.Integral.Lebesgue.Map
{α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {f : β → ENNReal} {g : α → β} (hf : Measurable f) (hg : Measurable g) : ∫⁻ (a : β), f a ∂MeasureTheory.Measure.map g μ = ∫⁻ (a : α), f (g a) ∂μ - MeasureTheory.lintegral_comp 📋 Mathlib.MeasureTheory.Integral.Lebesgue.Map
{α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {f : β → ENNReal} {g : α → β} (hf : Measurable f) (hg : Measurable g) : MeasureTheory.lintegral μ (f ∘ g) = ∫⁻ (a : β), f a ∂MeasureTheory.Measure.map g μ - MeasureTheory.lintegral_map' 📋 Mathlib.MeasureTheory.Integral.Lebesgue.Map
{α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {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.setLIntegral_map 📋 Mathlib.MeasureTheory.Integral.Lebesgue.Map
{α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {f : β → ENNReal} {g : α → β} {s : Set β} (hs : MeasurableSet s) (hf : Measurable f) (hg : Measurable g) : ∫⁻ (y : β) in s, f y ∂MeasureTheory.Measure.map g μ = ∫⁻ (x : α) in g ⁻¹' s, f (g x) ∂μ - MeasureTheory.lintegral_map_equiv 📋 Mathlib.MeasureTheory.Integral.Lebesgue.Map
{α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} (f : β → ENNReal) (g : α ≃ᵐ β) : ∫⁻ (a : β), f a ∂MeasureTheory.Measure.map (⇑g) μ = ∫⁻ (a : α), f (g a) ∂μ - MeasureTheory.AEStronglyMeasurable.comp_measurable 📋 Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
{α : 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 : Measurable f) : MeasureTheory.AEStronglyMeasurable (g ∘ f) μ - MeasurableEmbedding.aestronglyMeasurable_map_iff 📋 Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
{α : Type u_1} {β : Type u_2} [TopologicalSpace β] {γ : Type u_5} {mγ : MeasurableSpace γ} {mα : MeasurableSpace α} {f : γ → α} {μ : MeasureTheory.Measure γ} (hf : MeasurableEmbedding f) {g : α → β} : MeasureTheory.AEStronglyMeasurable g (MeasureTheory.Measure.map f μ) ↔ MeasureTheory.AEStronglyMeasurable (g ∘ f) μ - MeasureTheory.AEStronglyMeasurable.comp_aemeasurable 📋 Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
{α : 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) μ - MeasurableEmbedding.mutuallySingular_map 📋 Mathlib.MeasureTheory.Measure.MutuallySingular
{α : Type u_1} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} {β : Type u_2} {x✝ : MeasurableSpace β} {f : α → β} (hf : MeasurableEmbedding f) (hμν : μ.MutuallySingular ν) : (MeasureTheory.Measure.map f μ).MutuallySingular (MeasureTheory.Measure.map f ν) - MeasureTheory.instIsZeroOrProbabilityMeasureMap 📋 Mathlib.MeasureTheory.Measure.Typeclasses.Probability
{α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [MeasurableSpace β] {μ : MeasureTheory.Measure α} [MeasureTheory.IsZeroOrProbabilityMeasure μ] {f : α → β} : MeasureTheory.IsZeroOrProbabilityMeasure (MeasureTheory.Measure.map f μ) - MeasureTheory.isProbabilityMeasure_map_up 📋 Mathlib.MeasureTheory.Measure.Typeclasses.Probability
{α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] : MeasureTheory.IsProbabilityMeasure (MeasureTheory.Measure.map ULift.up μ) - MeasureTheory.isProbabilityMeasure_map 📋 Mathlib.MeasureTheory.Measure.Typeclasses.Probability
{α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [MeasurableSpace β] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] {f : α → β} (hf : AEMeasurable f μ) : MeasureTheory.IsProbabilityMeasure (MeasureTheory.Measure.map f μ) - MeasureTheory.Measure.map_dirac 📋 Mathlib.MeasureTheory.Measure.Dirac
{α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {f : α → β} (hf : Measurable f) (a : α) : MeasureTheory.Measure.map f (MeasureTheory.Measure.dirac a) = MeasureTheory.Measure.dirac (f a) - MeasureTheory.Measure.map_const 📋 Mathlib.MeasureTheory.Measure.Dirac
{α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (μ : MeasureTheory.Measure α) (c : β) : MeasureTheory.Measure.map (fun x => c) μ = μ Set.univ • MeasureTheory.Measure.dirac c - MeasureTheory.Measure.map_eq_sum 📋 Mathlib.MeasureTheory.Measure.Dirac
{α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Countable β] [MeasurableSingletonClass β] (μ : MeasureTheory.Measure α) (f : α → β) (hf : Measurable f) : MeasureTheory.Measure.map f μ = MeasureTheory.Measure.sum fun b => μ (f ⁻¹' {b}) • MeasureTheory.Measure.dirac b - MeasureTheory.Measure.join_map_dirac 📋 Mathlib.MeasureTheory.Measure.GiryMonad
{α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α) : (MeasureTheory.Measure.map MeasureTheory.Measure.dirac μ).join = μ - MeasureTheory.Measure.measurable_map 📋 Mathlib.MeasureTheory.Measure.GiryMonad
{α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (f : α → β) (hf : Measurable f) : Measurable fun μ => MeasureTheory.Measure.map f μ - 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.join_map_map 📋 Mathlib.MeasureTheory.Measure.GiryMonad
{α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α → β} (hf : Measurable f) (μ : MeasureTheory.Measure (MeasureTheory.Measure α)) : (MeasureTheory.Measure.map (MeasureTheory.Measure.map f) μ).join = MeasureTheory.Measure.map f μ.join - MeasureTheory.Measure.join_map_join 📋 Mathlib.MeasureTheory.Measure.GiryMonad
{α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure (MeasureTheory.Measure (MeasureTheory.Measure α))) : (MeasureTheory.Measure.map MeasureTheory.Measure.join μ).join = μ.join.join - Continuous.isOpenPosMeasure_map 📋 Mathlib.MeasureTheory.Measure.OpenPos
{X : Type u_1} [TopologicalSpace X] {m : MeasurableSpace X} {μ : MeasureTheory.Measure X} [μ.IsOpenPosMeasure] [OpensMeasurableSpace X] {Z : Type u_3} [TopologicalSpace Z] [MeasurableSpace Z] [BorelSpace Z] {f : X → Z} (hf : Continuous f) (hf_surj : Function.Surjective f) : (MeasureTheory.Measure.map f μ).IsOpenPosMeasure - MeasureTheory.Measure.fst.eq_1 📋 Mathlib.MeasureTheory.Measure.Prod
{α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (ρ : MeasureTheory.Measure (α × β)) : ρ.fst = MeasureTheory.Measure.map Prod.fst ρ - MeasureTheory.Measure.snd.eq_1 📋 Mathlib.MeasureTheory.Measure.Prod
{α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (ρ : MeasureTheory.Measure (α × β)) : ρ.snd = MeasureTheory.Measure.map Prod.snd ρ - MeasureTheory.Measure.dirac_prod 📋 Mathlib.MeasureTheory.Measure.Prod
{α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] (x : α) : (MeasureTheory.Measure.dirac x).prod ν = MeasureTheory.Measure.map (Prod.mk x) ν - Measurable.map_prodMk_left 📋 Mathlib.MeasureTheory.Measure.Prod
{α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] : Measurable fun x => MeasureTheory.Measure.map (Prod.mk x) ν - Measurable.map_prod_mk_left 📋 Mathlib.MeasureTheory.Measure.Prod
{α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] : Measurable fun x => MeasureTheory.Measure.map (Prod.mk x) ν - MeasureTheory.Measure.fst_map_swap 📋 Mathlib.MeasureTheory.Measure.Prod
{α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {ρ : MeasureTheory.Measure (α × β)} : (MeasureTheory.Measure.map Prod.swap ρ).fst = ρ.snd - MeasureTheory.Measure.snd_map_swap 📋 Mathlib.MeasureTheory.Measure.Prod
{α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {ρ : MeasureTheory.Measure (α × β)} : (MeasureTheory.Measure.map Prod.swap ρ).snd = ρ.fst - MeasureTheory.Measure.prod_dirac 📋 Mathlib.MeasureTheory.Measure.Prod
{α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} [MeasureTheory.SFinite μ] (y : β) : μ.prod (MeasureTheory.Measure.dirac y) = MeasureTheory.Measure.map (fun x => (x, y)) μ - Measurable.map_prodMk_right 📋 Mathlib.MeasureTheory.Measure.Prod
{α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} [MeasureTheory.SFinite μ] : Measurable fun y => MeasureTheory.Measure.map (fun x => (x, y)) μ - Measurable.map_prod_mk_right 📋 Mathlib.MeasureTheory.Measure.Prod
{α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} [MeasureTheory.SFinite μ] : Measurable fun y => MeasureTheory.Measure.map (fun x => (x, y)) μ - MeasureTheory.Measure.fst_map_prodMk 📋 Mathlib.MeasureTheory.Measure.Prod
{α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] {X : α → β} {Y : α → γ} {μ : MeasureTheory.Measure α} (hY : Measurable Y) : (MeasureTheory.Measure.map (fun a => (X a, Y a)) μ).fst = MeasureTheory.Measure.map 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 : Measurable Y) : (MeasureTheory.Measure.map (fun a => (X a, Y a)) μ).fst = MeasureTheory.Measure.map X μ - MeasureTheory.Measure.prod_def 📋 Mathlib.MeasureTheory.Measure.Prod
{α : Type u_4} {β : Type u_5} [MeasurableSpace α] [MeasurableSpace β] (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure β) : μ.prod ν = μ.bind fun x => MeasureTheory.Measure.map (Prod.mk x) ν - MeasureTheory.Measure.snd_map_prodMk 📋 Mathlib.MeasureTheory.Measure.Prod
{α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] {X : α → β} {Y : α → γ} {μ : MeasureTheory.Measure α} (hX : Measurable X) : (MeasureTheory.Measure.map (fun a => (X a, Y a)) μ).snd = MeasureTheory.Measure.map Y μ - 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 : Measurable X) : (MeasureTheory.Measure.map (fun a => (X a, Y a)) μ).snd = MeasureTheory.Measure.map Y μ - MeasureTheory.Measure.fst_map_prodMk₀ 📋 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.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_prodMk₀ 📋 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 μ - 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 μ - MeasureTheory.Measure.prod_swap 📋 Mathlib.MeasureTheory.Measure.Prod
{α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] : MeasureTheory.Measure.map Prod.swap (μ.prod ν) = ν.prod μ - MeasureTheory.Measure.map_fst_prod 📋 Mathlib.MeasureTheory.Measure.Prod
{α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] : MeasureTheory.Measure.map Prod.fst (μ.prod ν) = ν Set.univ • μ - MeasureTheory.Measure.map_snd_prod 📋 Mathlib.MeasureTheory.Measure.Prod
{α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] : MeasureTheory.Measure.map Prod.snd (μ.prod ν) = μ Set.univ • ν - MeasureTheory.Measure.map_prod_map 📋 Mathlib.MeasureTheory.Measure.Prod
{α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] {δ : Type u_4} [MeasurableSpace δ] {f : α → β} {g : γ → δ} (μa : MeasureTheory.Measure α) (μc : MeasureTheory.Measure γ) [MeasureTheory.SFinite μa] [MeasureTheory.SFinite μc] (hf : Measurable f) (hg : Measurable g) : (MeasureTheory.Measure.map f μa).prod (MeasureTheory.Measure.map g μc) = MeasureTheory.Measure.map (Prod.map f g) (μa.prod μc) - MeasureTheory.MeasurePreserving.skew_product 📋 Mathlib.MeasureTheory.Measure.Prod
{α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] {δ : Type u_4} [MeasurableSpace δ] {μa : MeasureTheory.Measure α} {μb : MeasureTheory.Measure β} {μc : MeasureTheory.Measure γ} {μd : MeasureTheory.Measure δ} [MeasureTheory.SFinite μa] [MeasureTheory.SFinite μc] {f : α → β} (hf : MeasureTheory.MeasurePreserving f μa μb) {g : α → γ → δ} (hgm : Measurable (Function.uncurry g)) (hg : ∀ᵐ (a : α) ∂μa, MeasureTheory.Measure.map (g a) μc = μd) : MeasureTheory.MeasurePreserving (fun p => (f p.1, g p.1 p.2)) (μa.prod μc) (μb.prod μd) - MeasureTheory.Measure.prodAssoc_prod 📋 Mathlib.MeasureTheory.Measure.Prod
{α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} {τ : MeasureTheory.Measure γ} [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] [MeasureTheory.SFinite τ] : MeasureTheory.Measure.map (⇑MeasurableEquiv.prodAssoc) ((μ.prod ν).prod τ) = μ.prod (ν.prod τ) - MeasurableEmbedding.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 : MeasurableEmbedding f) : essSup g (MeasureTheory.Measure.map f μ) = essSup (g ∘ f) μ - 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) μ - MeasurableEmbedding.eLpNormEssSup_map_measure 📋 Mathlib.MeasureTheory.Function.LpSeminorm.Basic
{α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ε : Type u_7} [TopologicalSpace ε] [ContinuousENorm ε] {β : Type u_8} {mβ : MeasurableSpace β} {f : α → β} {g : β → ε} (hf : MeasurableEmbedding f) : MeasureTheory.eLpNormEssSup g (MeasureTheory.Measure.map f μ) = MeasureTheory.eLpNormEssSup (g ∘ f) μ - MeasurableEmbedding.eLpNorm_map_measure 📋 Mathlib.MeasureTheory.Function.LpSeminorm.Basic
{α : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {ε : Type u_7} [TopologicalSpace ε] [ContinuousENorm ε] {β : Type u_8} {mβ : MeasurableSpace β} {f : α → β} {g : β → ε} (hf : MeasurableEmbedding f) : MeasureTheory.eLpNorm g p (MeasureTheory.Measure.map f μ) = MeasureTheory.eLpNorm (g ∘ f) p μ - MeasurableEmbedding.memLp_map_measure_iff 📋 Mathlib.MeasureTheory.Function.LpSeminorm.Basic
{α : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {ε : Type u_7} [TopologicalSpace ε] [ContinuousENorm ε] {β : Type u_8} {mβ : MeasurableSpace β} {f : α → β} {g : β → ε} (hf : MeasurableEmbedding f) : MeasureTheory.MemLp g p (MeasureTheory.Measure.map f μ) ↔ MeasureTheory.MemLp (g ∘ f) p μ - MeasurableEmbedding.memℒp_map_measure_iff 📋 Mathlib.MeasureTheory.Function.LpSeminorm.Basic
{α : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {ε : Type u_7} [TopologicalSpace ε] [ContinuousENorm ε] {β : Type u_8} {mβ : MeasurableSpace β} {f : α → β} {g : β → ε} (hf : MeasurableEmbedding f) : MeasureTheory.MemLp g p (MeasureTheory.Measure.map f μ) ↔ MeasureTheory.MemLp (g ∘ f) p μ - MeasureTheory.MemLp.comp_of_map 📋 Mathlib.MeasureTheory.Function.LpSeminorm.Basic
{α : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {ε : Type u_7} [TopologicalSpace ε] [ContinuousENorm ε] {β : Type u_8} {mβ : MeasurableSpace β} {f : α → β} {g : β → ε} (hg : MeasureTheory.MemLp g p (MeasureTheory.Measure.map f μ)) (hf : AEMeasurable f μ) : MeasureTheory.MemLp (g ∘ f) p μ - MeasureTheory.Memℒp.comp_of_map 📋 Mathlib.MeasureTheory.Function.LpSeminorm.Basic
{α : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {ε : Type u_7} [TopologicalSpace ε] [ContinuousENorm ε] {β : Type u_8} {mβ : MeasurableSpace β} {f : α → β} {g : β → ε} (hg : MeasureTheory.MemLp g p (MeasureTheory.Measure.map f μ)) (hf : AEMeasurable f μ) : MeasureTheory.MemLp (g ∘ f) p μ - MeasureTheory.eLpNormEssSup_map_measure 📋 Mathlib.MeasureTheory.Function.LpSeminorm.Basic
{α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ε : Type u_7} [TopologicalSpace ε] [ContinuousENorm ε] {β : Type u_8} {mβ : MeasurableSpace β} {f : α → β} {g : β → ε} (hg : MeasureTheory.AEStronglyMeasurable g (MeasureTheory.Measure.map f μ)) (hf : AEMeasurable f μ) : MeasureTheory.eLpNormEssSup g (MeasureTheory.Measure.map f μ) = MeasureTheory.eLpNormEssSup (g ∘ f) μ - MeasureTheory.eLpNorm_map_measure 📋 Mathlib.MeasureTheory.Function.LpSeminorm.Basic
{α : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {ε : Type u_7} [TopologicalSpace ε] [ContinuousENorm ε] {β : Type u_8} {mβ : MeasurableSpace β} {f : α → β} {g : β → ε} (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.memLp_map_measure_iff 📋 Mathlib.MeasureTheory.Function.LpSeminorm.Basic
{α : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {ε : Type u_7} [TopologicalSpace ε] [ContinuousENorm ε] {β : Type u_8} {mβ : MeasurableSpace β} {f : α → β} {g : β → ε} (hg : MeasureTheory.AEStronglyMeasurable g (MeasureTheory.Measure.map f μ)) (hf : AEMeasurable f μ) : MeasureTheory.MemLp g p (MeasureTheory.Measure.map f μ) ↔ MeasureTheory.MemLp (g ∘ f) p μ - MeasureTheory.memℒp_map_measure_iff 📋 Mathlib.MeasureTheory.Function.LpSeminorm.Basic
{α : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {ε : Type u_7} [TopologicalSpace ε] [ContinuousENorm ε] {β : Type u_8} {mβ : MeasurableSpace β} {f : α → β} {g : β → ε} (hg : MeasureTheory.AEStronglyMeasurable g (MeasureTheory.Measure.map f μ)) (hf : AEMeasurable f μ) : MeasureTheory.MemLp g p (MeasureTheory.Measure.map f μ) ↔ MeasureTheory.MemLp (g ∘ f) p μ - MeasurableEquiv.memLp_map_measure_iff 📋 Mathlib.MeasureTheory.Function.LpSeminorm.Basic
{α : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {ε : Type u_7} [TopologicalSpace ε] [ContinuousENorm ε] {β : Type u_8} {mβ : MeasurableSpace β} {g : β → ε} (f : α ≃ᵐ β) : MeasureTheory.MemLp g p (MeasureTheory.Measure.map (⇑f) μ) ↔ MeasureTheory.MemLp (g ∘ ⇑f) p μ - MeasurableEquiv.memℒp_map_measure_iff 📋 Mathlib.MeasureTheory.Function.LpSeminorm.Basic
{α : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {ε : Type u_7} [TopologicalSpace ε] [ContinuousENorm ε] {β : Type u_8} {mβ : MeasurableSpace β} {g : β → ε} (f : α ≃ᵐ β) : MeasureTheory.MemLp g p (MeasureTheory.Measure.map (⇑f) μ) ↔ MeasureTheory.MemLp (g ∘ ⇑f) p μ - MeasureTheory.Integrable.comp_measurable 📋 Mathlib.MeasureTheory.Function.L1Space.Integrable
{α : Type u_1} {ε : Type u_5} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace ε] [ContinuousENorm ε] {α' : Type u_8} [MeasurableSpace α'] {f : α → α'} {g : α' → ε} (hg : MeasureTheory.Integrable g (MeasureTheory.Measure.map f μ)) (hf : Measurable f) : MeasureTheory.Integrable (g ∘ f) μ - MeasurableEmbedding.integrable_map_iff 📋 Mathlib.MeasureTheory.Function.L1Space.Integrable
{α : Type u_1} {δ : Type u_4} {ε : Type u_5} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasurableSpace δ] [TopologicalSpace ε] [ContinuousENorm ε] {f : α → δ} (hf : MeasurableEmbedding f) {g : δ → ε} : MeasureTheory.Integrable g (MeasureTheory.Measure.map f μ) ↔ MeasureTheory.Integrable (g ∘ f) μ - MeasureTheory.Integrable.comp_aemeasurable 📋 Mathlib.MeasureTheory.Function.L1Space.Integrable
{α : Type u_1} {ε : Type u_5} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace ε] [ContinuousENorm ε] {α' : Type u_8} [MeasurableSpace α'] {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.Integrable
{α : Type u_1} {ε : Type u_5} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace ε] [ContinuousENorm ε] {α' : Type u_8} [MeasurableSpace α'] {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.integrable_map_equiv 📋 Mathlib.MeasureTheory.Function.L1Space.Integrable
{α : Type u_1} {δ : Type u_4} {ε : Type u_5} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasurableSpace δ] [TopologicalSpace ε] [ContinuousENorm ε] (f : α ≃ᵐ δ) (g : δ → ε) : MeasureTheory.Integrable g (MeasureTheory.Measure.map (⇑f) μ) ↔ MeasureTheory.Integrable (g ∘ ⇑f) μ - MeasureTheory.map_measureReal_apply 📋 Mathlib.MeasureTheory.Measure.Real
{α : Type u_1} {β : Type u_2} {x✝ : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasurableSpace β] {f : α → β} (hf : Measurable f) {s : Set β} (hs : MeasurableSet s) : (MeasureTheory.Measure.map f μ).real s = μ.real (f ⁻¹' s) - MeasurableEmbedding.integrableAtFilter_map_iff 📋 Mathlib.MeasureTheory.Integral.IntegrableOn
{α : Type u_1} {β : Type u_2} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {l : Filter α} [MeasurableSpace β] {e : α → β} (he : MeasurableEmbedding e) {f : β → E} : MeasureTheory.IntegrableAtFilter f (Filter.map e l) (MeasureTheory.Measure.map e μ) ↔ MeasureTheory.IntegrableAtFilter (f ∘ e) l μ - MeasurableEmbedding.integrableOn_map_iff 📋 Mathlib.MeasureTheory.Integral.IntegrableOn
{α : Type u_1} {β : Type u_2} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] [MeasurableSpace β] {e : α → β} (he : MeasurableEmbedding e) {f : β → E} {μ : MeasureTheory.Measure α} {s : Set β} : MeasureTheory.IntegrableOn f s (MeasureTheory.Measure.map e μ) ↔ MeasureTheory.IntegrableOn (f ∘ e) (e ⁻¹' s) μ - MeasureTheory.integrableOn_map_equiv 📋 Mathlib.MeasureTheory.Integral.IntegrableOn
{α : Type u_1} {β : Type u_2} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] [MeasurableSpace β] (e : α ≃ᵐ β) {f : β → E} {μ : MeasureTheory.Measure α} {s : Set β} : MeasureTheory.IntegrableOn f s (MeasureTheory.Measure.map (⇑e) μ) ↔ MeasureTheory.IntegrableOn (f ∘ ⇑e) (⇑e ⁻¹' s) μ - MeasureTheory.locallyIntegrable_map_homeomorph 📋 Mathlib.MeasureTheory.Function.LocallyIntegrable
{X : Type u_1} {Y : Type u_2} {E : Type u_3} [MeasurableSpace X] [TopologicalSpace X] [MeasurableSpace Y] [TopologicalSpace Y] [NormedAddCommGroup E] [BorelSpace X] [BorelSpace Y] (e : X ≃ₜ Y) {f : Y → E} {μ : MeasureTheory.Measure X} : MeasureTheory.LocallyIntegrable f (MeasureTheory.Measure.map (⇑e) μ) ↔ MeasureTheory.LocallyIntegrable (f ∘ ⇑e) μ - MeasurableEmbedding.integral_map 📋 Mathlib.MeasureTheory.Integral.Bochner.Basic
{α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] [NormedSpace ℝ G] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_7} {x✝ : MeasurableSpace β} {f : α → β} (hf : MeasurableEmbedding f) (g : β → G) : ∫ (y : β), g y ∂MeasureTheory.Measure.map f μ = ∫ (x : α), g (f x) ∂μ - Topology.IsClosedEmbedding.integral_map 📋 Mathlib.MeasureTheory.Integral.Bochner.Basic
{α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] [NormedSpace ℝ G] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_7} [TopologicalSpace α] [BorelSpace α] [TopologicalSpace β] [MeasurableSpace β] [BorelSpace β] {φ : α → β} (hφ : Topology.IsClosedEmbedding φ) (f : β → G) : ∫ (y : β), f y ∂MeasureTheory.Measure.map φ μ = ∫ (x : α), f (φ x) ∂μ - MeasureTheory.integral_map_of_stronglyMeasurable 📋 Mathlib.MeasureTheory.Integral.Bochner.Basic
{α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] [NormedSpace ℝ G] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_7} [MeasurableSpace β] {φ : α → β} (hφ : Measurable φ) {f : β → G} (hfm : MeasureTheory.StronglyMeasurable f) : ∫ (y : β), f y ∂MeasureTheory.Measure.map φ μ = ∫ (x : α), f (φ x) ∂μ - MeasureTheory.integral_map 📋 Mathlib.MeasureTheory.Integral.Bochner.Basic
{α : 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.integral_map_equiv 📋 Mathlib.MeasureTheory.Integral.Bochner.Basic
{α : Type u_1} {G : Type u_5} [NormedAddCommGroup G] [NormedSpace ℝ G] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_7} [MeasurableSpace β] (e : α ≃ᵐ β) (f : β → G) : ∫ (y : β), f y ∂MeasureTheory.Measure.map (⇑e) μ = ∫ (x : α), f (e x) ∂μ - MeasurableEmbedding.setIntegral_map 📋 Mathlib.MeasureTheory.Integral.Bochner.Set
{X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] {μ : MeasureTheory.Measure X} {Y : Type u_5} {x✝ : MeasurableSpace Y} {f : X → Y} (hf : MeasurableEmbedding f) (g : Y → E) (s : Set Y) : ∫ (y : Y) in s, g y ∂MeasureTheory.Measure.map f μ = ∫ (x : X) in f ⁻¹' s, g (f x) ∂μ - Topology.IsClosedEmbedding.setIntegral_map 📋 Mathlib.MeasureTheory.Integral.Bochner.Set
{X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] {μ : MeasureTheory.Measure X} [TopologicalSpace X] [BorelSpace X] {Y : Type u_5} [MeasurableSpace Y] [TopologicalSpace Y] [BorelSpace Y] {g : X → Y} {f : Y → E} (s : Set Y) (hg : Topology.IsClosedEmbedding g) : ∫ (y : Y) in s, f y ∂MeasureTheory.Measure.map g μ = ∫ (x : X) in g ⁻¹' s, f (g x) ∂μ - MeasureTheory.setIntegral_map 📋 Mathlib.MeasureTheory.Integral.Bochner.Set
{X : Type u_1} {E : Type u_3} {mX : 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.setIntegral_map_equiv 📋 Mathlib.MeasureTheory.Integral.Bochner.Set
{X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] {μ : MeasureTheory.Measure X} {Y : Type u_5} [MeasurableSpace Y] (e : X ≃ᵐ Y) (f : Y → E) (s : Set Y) : ∫ (y : Y) in s, f y ∂MeasureTheory.Measure.map (⇑e) μ = ∫ (x : X) in ⇑e ⁻¹' s, f (e x) ∂μ - MeasureTheory.IsAddFundamentalDomain.addQuotientMeasureEqMeasurePreimage_addQuotientMeasure 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] {ν : MeasureTheory.Measure α} [MeasureTheory.VAddInvariantMeasure G α ν] [Countable G] [MeasurableSpace G] [MeasurableVAdd G α] {s : Set α} (fund_dom_s : MeasureTheory.IsAddFundamentalDomain G s ν) : MeasureTheory.AddQuotientMeasureEqMeasurePreimage ν (MeasureTheory.Measure.map (Quotient.mk (AddAction.orbitRel G α)) (ν.restrict s)) - MeasureTheory.IsFundamentalDomain.quotientMeasureEqMeasurePreimage_quotientMeasure 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] {ν : MeasureTheory.Measure α} [MeasureTheory.SMulInvariantMeasure G α ν] [Countable G] [MeasurableSpace G] [MeasurableSMul G α] {s : Set α} (fund_dom_s : MeasureTheory.IsFundamentalDomain G s ν) : MeasureTheory.QuotientMeasureEqMeasurePreimage ν (MeasureTheory.Measure.map (Quotient.mk (MulAction.orbitRel G α)) (ν.restrict s)) - MeasureTheory.IsAddFundamentalDomain.addProjection_respects_measure 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] {ν : MeasureTheory.Measure α} (μ : MeasureTheory.Measure (Quotient (AddAction.orbitRel G α))) [i : MeasureTheory.AddQuotientMeasureEqMeasurePreimage ν μ] {t : Set α} (fund_dom_t : MeasureTheory.IsAddFundamentalDomain G t ν) : μ = MeasureTheory.Measure.map (Quotient.mk (AddAction.orbitRel G α)) (ν.restrict t) - MeasureTheory.IsFundamentalDomain.projection_respects_measure 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] {ν : MeasureTheory.Measure α} (μ : MeasureTheory.Measure (Quotient (MulAction.orbitRel G α))) [i : MeasureTheory.QuotientMeasureEqMeasurePreimage ν μ] {t : Set α} (fund_dom_t : MeasureTheory.IsFundamentalDomain G t ν) : μ = MeasureTheory.Measure.map (Quotient.mk (MulAction.orbitRel G α)) (ν.restrict t) - MeasureTheory.AddQuotientMeasureEqMeasurePreimage.addProjection_respects_measure' 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{G : Type u_1} {α : Type u_3} {inst✝ : AddGroup G} {inst✝¹ : AddAction G α} {inst✝² : MeasurableSpace α} {ν : autoParam (MeasureTheory.Measure α) _auto✝} {μ : MeasureTheory.Measure (Quotient (AddAction.orbitRel G α))} [self : MeasureTheory.AddQuotientMeasureEqMeasurePreimage ν μ] (t : Set α) : MeasureTheory.IsAddFundamentalDomain G t ν → μ = MeasureTheory.Measure.map (Quotient.mk (AddAction.orbitRel G α)) (MeasureTheory.Measure.restrict ν t) - MeasureTheory.AddQuotientMeasureEqMeasurePreimage.mk 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] {ν : autoParam (MeasureTheory.Measure α) _auto✝} {μ : MeasureTheory.Measure (Quotient (AddAction.orbitRel G α))} (addProjection_respects_measure' : ∀ (t : Set α), MeasureTheory.IsAddFundamentalDomain G t ν → μ = MeasureTheory.Measure.map (Quotient.mk (AddAction.orbitRel G α)) (MeasureTheory.Measure.restrict ν t)) : MeasureTheory.AddQuotientMeasureEqMeasurePreimage ν μ - MeasureTheory.QuotientMeasureEqMeasurePreimage.mk 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] {ν : autoParam (MeasureTheory.Measure α) _auto✝} {μ : MeasureTheory.Measure (Quotient (MulAction.orbitRel G α))} (projection_respects_measure' : ∀ (t : Set α), MeasureTheory.IsFundamentalDomain G t ν → μ = MeasureTheory.Measure.map (Quotient.mk (MulAction.orbitRel G α)) (MeasureTheory.Measure.restrict ν t)) : MeasureTheory.QuotientMeasureEqMeasurePreimage ν μ - MeasureTheory.QuotientMeasureEqMeasurePreimage.projection_respects_measure' 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{G : Type u_1} {α : Type u_3} {inst✝ : Group G} {inst✝¹ : MulAction G α} {inst✝² : MeasurableSpace α} {ν : autoParam (MeasureTheory.Measure α) _auto✝} {μ : MeasureTheory.Measure (Quotient (MulAction.orbitRel G α))} [self : MeasureTheory.QuotientMeasureEqMeasurePreimage ν μ] (t : Set α) : MeasureTheory.IsFundamentalDomain G t ν → μ = MeasureTheory.Measure.map (Quotient.mk (MulAction.orbitRel G α)) (MeasureTheory.Measure.restrict ν t) - MeasureTheory.IsAddFundamentalDomain.addQuotientMeasureEqMeasurePreimage 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] {ν : MeasureTheory.Measure α} [MeasureTheory.VAddInvariantMeasure G α ν] [Countable G] [MeasurableSpace G] [MeasurableVAdd G α] {μ : MeasureTheory.Measure (Quotient (AddAction.orbitRel G α))} {s : Set α} (fund_dom_s : MeasureTheory.IsAddFundamentalDomain G s ν) (h : μ = MeasureTheory.Measure.map (Quotient.mk (AddAction.orbitRel G α)) (ν.restrict s)) : MeasureTheory.AddQuotientMeasureEqMeasurePreimage ν μ - MeasureTheory.IsFundamentalDomain.quotientMeasureEqMeasurePreimage 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [MeasurableSpace α] {ν : MeasureTheory.Measure α} [MeasureTheory.SMulInvariantMeasure G α ν] [Countable G] [MeasurableSpace G] [MeasurableSMul G α] {μ : MeasureTheory.Measure (Quotient (MulAction.orbitRel G α))} {s : Set α} (fund_dom_s : MeasureTheory.IsFundamentalDomain G s ν) (h : μ = MeasureTheory.Measure.map (Quotient.mk (MulAction.orbitRel G α)) (ν.restrict s)) : MeasureTheory.QuotientMeasureEqMeasurePreimage ν μ - MeasureTheory.addMeasure_map_restrict_apply 📋 Mathlib.MeasureTheory.Group.FundamentalDomain
{G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [MeasurableSpace α] (μ : MeasureTheory.Measure α) (s : Set α) {U : Set (Quotient (AddAction.orbitRel G α))} (meas_U : MeasurableSet U) : (MeasureTheory.Measure.map (Quotient.mk (AddAction.orbitRel G α)) (μ.restrict s)) U = μ (Quotient.mk (AddAction.orbitRel G α) ⁻¹' U ∩ 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:
By constant:
🔍Real.sin
finds all lemmas whose statement somehow mentions the sine function.By lemma name substring:
🔍"differ"
finds all lemmas that have"differ"somewhere in their lemma name.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 ?aIf 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 ?bBy 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 findtsum_lt_tsumeven though the hypothesisf i < g iis 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 19971e9 serving mathlib revision bce1d65