ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>G : Type u_1<VAR>Group G<VAR>MeasurableSpace G<VAR>TopologicalSpace G<VAR>TopologicalGroup G<VAR>BorelSpace G<VAR>μ : MeasureTheory.Measure G<VAR>Γ : Subgroup G<VAR>𝓕 : Set G<VAR>h𝓕 : MeasureTheory.IsFundamentalDomain (↥Γ.op) 𝓕 μ<VAR>Countable ↥Γ<VAR>MeasurableSpace (G ⧸ Γ)<VAR>BorelSpace (G ⧸ Γ)<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>μ.IsMulRightInvariant<VAR>f : G → E<VAR>hf₁ : MeasureTheory.Integrable f μ<VAR>hf₂ : MeasureTheory.AEStronglyMeasurable (QuotientGroup.automorphize f) (MeasureTheory.Measure.map QuotientGroup.mk (μ.restrict 𝓕))<GOAL>∫ (x : G), f x ∂μ = ∫ (x : G ⧸ Γ), QuotientGroup.automorphize f x ∂MeasureTheory.Measure.map QuotientGroup.mk (μ.restrict 𝓕)
<VAR>G : Type u_1<VAR>Group G<VAR>MeasurableSpace G<VAR>TopologicalSpace G<VAR>TopologicalGroup G<VAR>BorelSpace G<VAR>μ : MeasureTheory.Measure G<VAR>Γ : Subgroup G<VAR>𝓕 : Set G<VAR>h𝓕 : MeasureTheory.IsFundamentalDomain (↥Γ.op) 𝓕 μ<VAR>Countable ↥Γ<VAR>MeasurableSpace (G ⧸ Γ)<VAR>BorelSpace (G ⧸ Γ)<VAR>K : Type u_2<VAR>NormedField K<VAR>NormedSpace ℝ K<VAR>μ.IsMulRightInvariant<VAR>f : G → K<VAR>f_ℒ_1 : MeasureTheory.Integrable f μ<VAR>g : G ⧸ Γ → K<VAR>hg : MeasureTheory.AEStronglyMeasurable g (MeasureTheory.Measure.map QuotientGroup.mk (μ.restrict 𝓕))<VAR>g_ℒ_infinity : essSup (fun x => ↑‖g x‖₊) (MeasureTheory.Measure.map QuotientGroup.mk (μ.restrict 𝓕)) ≠ ⊤<VAR>F_ae_measurable : MeasureTheory.AEStronglyMeasurable (QuotientGroup.automorphize f) (MeasureTheory.Measure.map QuotientGroup.mk (μ.restrict 𝓕))<GOAL>∫ (x : G), g ↑x * f x ∂μ = ∫ (x : G ⧸ Γ), g x * QuotientGroup.automorphize f x ∂MeasureTheory.Measure.map QuotientGroup.mk (μ.restrict 𝓕)
<VAR>G' : Type u_1<VAR>AddGroup G'<VAR>MeasurableSpace G'<VAR>TopologicalSpace G'<VAR>TopologicalAddGroup G'<VAR>BorelSpace G'<VAR>μ' : MeasureTheory.Measure G'<VAR>Γ' : AddSubgroup G'<VAR>Countable ↥Γ'<VAR>MeasurableSpace (G' ⧸ Γ')<VAR>BorelSpace (G' ⧸ Γ')<VAR>𝓕' : Set G'<VAR>K : Type u_2<VAR>NormedField K<VAR>NormedSpace ℝ K<VAR>μ'.IsAddRightInvariant<VAR>f : G' → K<VAR>f_ℒ_1 : MeasureTheory.Integrable f μ'<VAR>g : G' ⧸ Γ' → K<VAR>hg : MeasureTheory.AEStronglyMeasurable g (MeasureTheory.Measure.map QuotientAddGroup.mk (μ'.restrict 𝓕'))<VAR>g_ℒ_infinity : essSup (fun x => ↑‖g x‖₊) (MeasureTheory.Measure.map QuotientAddGroup.mk (μ'.restrict 𝓕')) ≠ ⊤<VAR>F_ae_measurable : MeasureTheory.AEStronglyMeasurable (QuotientAddGroup.automorphize f) (MeasureTheory.Measure.map QuotientAddGroup.mk (μ'.restrict 𝓕'))<VAR>h𝓕 : MeasureTheory.IsAddFundamentalDomain (↥Γ'.op) 𝓕' μ'<GOAL>∫ (x : G'), g ↑x * f x ∂μ' = ∫ (x : G' ⧸ Γ'), g x * QuotientAddGroup.automorphize f x ∂MeasureTheory.Measure.map QuotientAddGroup.mk (μ'.restrict 𝓕')
<VAR>Ω : Type u_1<VAR>TopologicalSpace Ω<VAR>MeasurableSpace Ω<VAR>OpensMeasurableSpace Ω<VAR>ι : Type u_2<VAR>L : Filter ι<VAR>L.IsCountablyGenerated<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>fs : ι → Ω →ᵇ ℝ≥0<VAR>c : ℝ≥0<VAR>fs_le_const : ∀ᶠ (i : ι) in L, ∀ᵐ (ω : Ω) ∂μ, (fs i) ω ≤ c<VAR>f : Ω → ℝ≥0<VAR>fs_lim : ∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun i => (fs i) ω) L (𝓝 (f ω))<GOAL>Filter.Tendsto (fun i => ∫⁻ (ω : Ω), ↑((fs i) ω) ∂μ) L (𝓝 (∫⁻ (ω : Ω), ↑(f ω) ∂μ))
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>ι : Type u_2<VAR>L : Filter ι<VAR>L.IsCountablyGenerated<VAR>TopologicalSpace Ω<VAR>OpensMeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>c : ℝ≥0<VAR>E : Set Ω<VAR>E_mble : MeasurableSet E<VAR>fs : ι → Ω →ᵇ ℝ≥0<VAR>fs_bdd : ∀ᶠ (i : ι) in L, ∀ᵐ (ω : Ω) ∂μ, (fs i) ω ≤ c<VAR>fs_lim : ∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun i => (fs i) ω) L (𝓝 (E.indicator (fun x => 1) ω))<GOAL>Filter.Tendsto (fun n => ∫⁻ (ω : Ω), ↑((fs n) ω) ∂μ) L (𝓝 (μ E))
<VAR>Ω : Type u_1<VAR>TopologicalSpace Ω<VAR>MeasurableSpace Ω<VAR>OpensMeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>c : ℝ≥0<VAR>E : Set Ω<VAR>E_mble : MeasurableSet E<VAR>fs : ℕ → Ω →ᵇ ℝ≥0<VAR>fs_bdd : ∀ (n : ℕ) (ω : Ω), (fs n) ω ≤ c<VAR>fs_lim : Filter.Tendsto (fun n ω => (fs n) ω) Filter.atTop (𝓝 (E.indicator fun x => 1))<GOAL>Filter.Tendsto (fun n => ∫⁻ (ω : Ω), ↑((fs n) ω) ∂μ) Filter.atTop (𝓝 (μ E))
<VAR>Ω : Type u_2<VAR>MeasurableSpace Ω<VAR>PseudoEMetricSpace Ω<VAR>OpensMeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>F : Set Ω<VAR>F_closed : IsClosed F<VAR>δs : ℕ → ℝ<VAR>δs_pos : ∀ (n : ℕ), 0 < δs n<VAR>δs_lim : Filter.Tendsto δs Filter.atTop (𝓝 0)<GOAL>Filter.Tendsto (fun n => ∫⁻ (ω : Ω), ↑((thickenedIndicator ⋯ F) ω) ∂μ) Filter.atTop (𝓝 (μ F))
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>self : HasOuterApproxClosed X<VAR>F : Set X<GOAL>IsClosed F → ∃ fseq, (∀ (n : ℕ) (x : X), (fseq n) x ≤ 1) ∧ (∀ (n : ℕ), ∀ x ∈ F, 1 ≤ (fseq n) x) ∧ Filter.Tendsto (fun n x => (fseq n) x) Filter.atTop (𝓝 (F.indicator fun x => 1))
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>HasOuterApproxClosed X<VAR>F : Set X<VAR>hF : IsClosed F<VAR>n : ℕ<VAR>x : X<GOAL>(hF.apprSeq n) x ≤ 1
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>HasOuterApproxClosed X<VAR>F : Set X<VAR>hF : IsClosed F<VAR>n : ℕ<VAR>x : X<VAR>hxF : x ∈ F<GOAL>(hF.apprSeq n) x = 1
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>HasOuterApproxClosed X<VAR>F : Set X<VAR>hF : IsClosed F<GOAL>Filter.Tendsto (fun n x => (hF.apprSeq n) x) Filter.atTop (𝓝 (F.indicator fun x => 1))
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>HasOuterApproxClosed X<VAR>F : Set X<VAR>hF : IsClosed F<VAR>n : ℕ<GOAL>(F.indicator fun x => 1) ≤ ⇑(hF.apprSeq n)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>HasOuterApproxClosed X<VAR>F : Set X<VAR>hF : IsClosed F<VAR>MeasurableSpace X<VAR>OpensMeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>n : ℕ<GOAL>μ F ≤ ∫⁻ (x : X), ↑((hF.apprSeq n) x) ∂μ
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>HasOuterApproxClosed X<VAR>F : Set X<VAR>hF : IsClosed F<VAR>MeasurableSpace X<VAR>OpensMeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>MeasureTheory.IsFiniteMeasure μ<GOAL>Filter.Tendsto (fun n => ∫⁻ (x : X), ↑((hF.apprSeq n) x) ∂μ) Filter.atTop (𝓝 (μ F))
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>TopologicalSpace Ω<VAR>HasOuterApproxClosed Ω<VAR>OpensMeasurableSpace Ω<VAR>μ ν : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>h : ∀ (f : Ω →ᵇ ℝ≥0), ∫⁻ (x : Ω), ↑(f x) ∂μ = ∫⁻ (x : Ω), ↑(f x) ∂ν<VAR>F : Set Ω<VAR>F_closed : IsClosed F<GOAL>μ F = ν F
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>TopologicalSpace Ω<VAR>HasOuterApproxClosed Ω<VAR>BorelSpace Ω<VAR>μ ν : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>h : ∀ (f : Ω →ᵇ ℝ≥0), ∫⁻ (x : Ω), ↑(f x) ∂μ = ∫⁻ (x : Ω), ↑(f x) ∂ν<GOAL>μ = ν
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>self : MeasureTheory.Content G<VAR>K₁ K₂ : TopologicalSpace.Compacts G<GOAL>↑K₁ ⊆ ↑K₂ → self.toFun K₁ ≤ self.toFun K₂
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>self : MeasureTheory.Content G<VAR>K₁ K₂ : TopologicalSpace.Compacts G<GOAL>self.toFun (K₁ ⊔ K₂) ≤ self.toFun K₁ + self.toFun K₂
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>self : MeasureTheory.Content G<VAR>K₁ K₂ : TopologicalSpace.Compacts G<GOAL>Disjoint ↑K₁ ↑K₂ → IsClosed ↑K₁ → IsClosed ↑K₂ → self.toFun (K₁ ⊔ K₂) = self.toFun K₁ + self.toFun K₂
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>μ : MeasureTheory.Content G<VAR>K : TopologicalSpace.Compacts G<GOAL>(fun s => ↑(μ.toFun s)) K = ↑(μ.toFun K)
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>μ : MeasureTheory.Content G<VAR>K₁ K₂ : TopologicalSpace.Compacts G<VAR>h : ↑K₁ ⊆ ↑K₂<GOAL>(fun s => ↑(μ.toFun s)) K₁ ≤ (fun s => ↑(μ.toFun s)) K₂
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>μ : MeasureTheory.Content G<VAR>K₁ K₂ : TopologicalSpace.Compacts G<VAR>h : Disjoint ↑K₁ ↑K₂<VAR>h₁ : IsClosed ↑K₁<VAR>h₂ : IsClosed ↑K₂<GOAL>(fun s => ↑(μ.toFun s)) (K₁ ⊔ K₂) = (fun s => ↑(μ.toFun s)) K₁ + (fun s => ↑(μ.toFun s)) K₂
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>μ : MeasureTheory.Content G<VAR>K₁ K₂ : TopologicalSpace.Compacts G<GOAL>(fun s => ↑(μ.toFun s)) (K₁ ⊔ K₂) ≤ (fun s => ↑(μ.toFun s)) K₁ + (fun s => ↑(μ.toFun s)) K₂
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>μ : MeasureTheory.Content G<VAR>K : TopologicalSpace.Compacts G<GOAL>(fun s => ↑(μ.toFun s)) K < ⊤
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>μ : MeasureTheory.Content G<GOAL>(fun s => ↑(μ.toFun s)) ⊥ = 0
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>μ : MeasureTheory.Content G<VAR>K : TopologicalSpace.Compacts G<VAR>U : TopologicalSpace.Opens G<VAR>h2 : ↑K ⊆ ↑U<GOAL>(fun s => ↑(μ.toFun s)) K ≤ μ.innerContent U
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>μ : MeasureTheory.Content G<VAR>U : TopologicalSpace.Opens G<VAR>K : TopologicalSpace.Compacts G<VAR>h2 : ↑U ⊆ ↑K<GOAL>μ.innerContent U ≤ (fun s => ↑(μ.toFun s)) K
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>μ : MeasureTheory.Content G<VAR>K : Set G<VAR>h1K : IsCompact K<VAR>h2K : IsOpen K<GOAL>μ.innerContent { carrier := K, is_open' := h2K } = (fun s => ↑(μ.toFun s)) { carrier := K, isCompact' := h1K }
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>μ : MeasureTheory.Content G<GOAL>μ.innerContent ⊥ = 0
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>μ : MeasureTheory.Content G<VAR>U V : Set G<VAR>hU : IsOpen U<VAR>hV : IsOpen V<VAR>h2 : U ⊆ V<GOAL>μ.innerContent { carrier := U, is_open' := hU } ≤ μ.innerContent { carrier := V, is_open' := hV }
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>μ : MeasureTheory.Content G<VAR>U : TopologicalSpace.Opens G<VAR>hU : μ.innerContent U ≠ ⊤<VAR>ε : ℝ≥0<VAR>hε : ε ≠ 0<GOAL>∃ K, ↑K ⊆ ↑U ∧ μ.innerContent U ≤ (fun s => ↑(μ.toFun s)) K + ↑ε
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>μ : MeasureTheory.Content G<VAR>R1Space G<VAR>U : ℕ → TopologicalSpace.Opens G<GOAL>μ.innerContent (⨆ i, U i) ≤ ∑' (i : ℕ), μ.innerContent (U i)
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>μ : MeasureTheory.Content G<VAR>R1Space G<VAR>U : ℕ → Set G<VAR>hU : ∀ (i : ℕ), IsOpen (U i)<GOAL>μ.innerContent { carrier := ⋃ i, U i, is_open' := ⋯ } ≤ ∑' (i : ℕ), μ.innerContent { carrier := U i, is_open' := ⋯ }
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>μ : MeasureTheory.Content G<VAR>f : G ≃ₜ G<VAR>h : ∀ ⦃K : TopologicalSpace.Compacts G⦄, (fun s => ↑(μ.toFun s)) (TopologicalSpace.Compacts.map ⇑f ⋯ K) = (fun s => ↑(μ.toFun s)) K<VAR>U : TopologicalSpace.Opens G<GOAL>μ.innerContent ((TopologicalSpace.Opens.comap f.toContinuousMap) U) = μ.innerContent U
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>μ : MeasureTheory.Content G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>h : ∀ (g : G) {K : TopologicalSpace.Compacts G}, (fun s => ↑(μ.toFun s)) (TopologicalSpace.Compacts.map (fun b => g + b) ⋯ K) = (fun s => ↑(μ.toFun s)) K<VAR>g : G<VAR>U : TopologicalSpace.Opens G<GOAL>μ.innerContent ((TopologicalSpace.Opens.comap (Homeomorph.addLeft g).toContinuousMap) U) = μ.innerContent U
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>μ : MeasureTheory.Content G<VAR>Group G<VAR>TopologicalGroup G<VAR>h : ∀ (g : G) {K : TopologicalSpace.Compacts G}, (fun s => ↑(μ.toFun s)) (TopologicalSpace.Compacts.map (fun b => g * b) ⋯ K) = (fun s => ↑(μ.toFun s)) K<VAR>g : G<VAR>U : TopologicalSpace.Opens G<GOAL>μ.innerContent ((TopologicalSpace.Opens.comap (Homeomorph.mulLeft g).toContinuousMap) U) = μ.innerContent U
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>μ : MeasureTheory.Content G<VAR>Group G<VAR>TopologicalGroup G<VAR>h3 : ∀ (g : G) {K : TopologicalSpace.Compacts G}, (fun s => ↑(μ.toFun s)) (TopologicalSpace.Compacts.map (fun b => g * b) ⋯ K) = (fun s => ↑(μ.toFun s)) K<VAR>K : TopologicalSpace.Compacts G<VAR>hK : (fun s => ↑(μ.toFun s)) K ≠ 0<VAR>U : TopologicalSpace.Opens G<VAR>hU : (↑U).Nonempty<GOAL>0 < μ.innerContent U
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>μ : MeasureTheory.Content G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>h3 : ∀ (g : G) {K : TopologicalSpace.Compacts G}, (fun s => ↑(μ.toFun s)) (TopologicalSpace.Compacts.map (fun b => g + b) ⋯ K) = (fun s => ↑(μ.toFun s)) K<VAR>K : TopologicalSpace.Compacts G<VAR>hK : (fun s => ↑(μ.toFun s)) K ≠ 0<VAR>U : TopologicalSpace.Opens G<VAR>hU : (↑U).Nonempty<GOAL>0 < μ.innerContent U
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>μ : MeasureTheory.Content G<VAR>R1Space G<VAR>U : TopologicalSpace.Opens G<GOAL>μ.outerMeasure ↑U = μ.innerContent U
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>μ : MeasureTheory.Content G<VAR>R1Space G<VAR>U : Set G<VAR>hU : IsOpen U<GOAL>μ.outerMeasure U = μ.innerContent { carrier := U, is_open' := hU }
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>μ : MeasureTheory.Content G<VAR>R1Space G<VAR>U : TopologicalSpace.Opens G<VAR>K : TopologicalSpace.Compacts G<VAR>hUK : ↑U ⊆ ↑K<GOAL>μ.outerMeasure ↑U ≤ (fun s => ↑(μ.toFun s)) K
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>μ : MeasureTheory.Content G<VAR>R1Space G<VAR>K : TopologicalSpace.Compacts G<GOAL>(fun s => ↑(μ.toFun s)) K ≤ μ.outerMeasure ↑K
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>μ : MeasureTheory.Content G<VAR>R1Space G<VAR>A : Set G<GOAL>μ.outerMeasure A = ⨅ U, ⨅ (hU : IsOpen U), ⨅ (_ : A ⊆ U), μ.innerContent { carrier := U, is_open' := hU }
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>μ : MeasureTheory.Content G<VAR>R1Space G<VAR>K : TopologicalSpace.Compacts G<GOAL>μ.outerMeasure (interior ↑K) ≤ (fun s => ↑(μ.toFun s)) K
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>μ : MeasureTheory.Content G<VAR>R1Space G<VAR>U : TopologicalSpace.Opens G<VAR>hU : μ.outerMeasure ↑U ≠ ⊤<VAR>ε : ℝ≥0<VAR>hε : ε ≠ 0<GOAL>∃ K, ↑K ⊆ ↑U ∧ μ.outerMeasure ↑U ≤ μ.outerMeasure ↑K + ↑ε
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>μ : MeasureTheory.Content G<VAR>R1Space G<VAR>A : Set G<VAR>hA : μ.outerMeasure A ≠ ⊤<VAR>ε : ℝ≥0<VAR>hε : ε ≠ 0<GOAL>∃ U, A ⊆ ↑U ∧ μ.outerMeasure ↑U ≤ μ.outerMeasure A + ↑ε
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>μ : MeasureTheory.Content G<VAR>R1Space G<VAR>f : G ≃ₜ G<VAR>h : ∀ ⦃K : TopologicalSpace.Compacts G⦄, (fun s => ↑(μ.toFun s)) (TopologicalSpace.Compacts.map ⇑f ⋯ K) = (fun s => ↑(μ.toFun s)) K<VAR>A : Set G<GOAL>μ.outerMeasure (⇑f ⁻¹' A) = μ.outerMeasure A
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>μ : MeasureTheory.Content G<VAR>R1Space G<VAR>WeaklyLocallyCompactSpace G<VAR>K : Set G<VAR>hK : IsCompact K<GOAL>μ.outerMeasure K < ⊤
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>μ : MeasureTheory.Content G<VAR>R1Space G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>h : ∀ (g : G) {K : TopologicalSpace.Compacts G}, (fun s => ↑(μ.toFun s)) (TopologicalSpace.Compacts.map (fun b => g + b) ⋯ K) = (fun s => ↑(μ.toFun s)) K<VAR>g : G<VAR>A : Set G<GOAL>μ.outerMeasure ((fun x => g + x) ⁻¹' A) = μ.outerMeasure A
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>μ : MeasureTheory.Content G<VAR>R1Space G<VAR>Group G<VAR>TopologicalGroup G<VAR>h : ∀ (g : G) {K : TopologicalSpace.Compacts G}, (fun s => ↑(μ.toFun s)) (TopologicalSpace.Compacts.map (fun b => g * b) ⋯ K) = (fun s => ↑(μ.toFun s)) K<VAR>g : G<VAR>A : Set G<GOAL>μ.outerMeasure ((fun x => g * x) ⁻¹' A) = μ.outerMeasure A
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>μ : MeasureTheory.Content G<VAR>R1Space G<VAR>A : Set G<GOAL>MeasurableSet A ↔ ∀ (U : TopologicalSpace.Opens G), μ.outerMeasure (↑U ∩ A) + μ.outerMeasure (↑U \ A) ≤ μ.outerMeasure ↑U
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>μ : MeasureTheory.Content G<VAR>R1Space G<VAR>Group G<VAR>TopologicalGroup G<VAR>h3 : ∀ (g : G) {K : TopologicalSpace.Compacts G}, (fun s => ↑(μ.toFun s)) (TopologicalSpace.Compacts.map (fun b => g * b) ⋯ K) = (fun s => ↑(μ.toFun s)) K<VAR>K : TopologicalSpace.Compacts G<VAR>hK : (fun s => ↑(μ.toFun s)) K ≠ 0<VAR>U : Set G<VAR>h1U : IsOpen U<VAR>h2U : U.Nonempty<GOAL>0 < μ.outerMeasure U
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>μ : MeasureTheory.Content G<VAR>R1Space G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>h3 : ∀ (g : G) {K : TopologicalSpace.Compacts G}, (fun s => ↑(μ.toFun s)) (TopologicalSpace.Compacts.map (fun b => g + b) ⋯ K) = (fun s => ↑(μ.toFun s)) K<VAR>K : TopologicalSpace.Compacts G<VAR>hK : (fun s => ↑(μ.toFun s)) K ≠ 0<VAR>U : Set G<VAR>h1U : IsOpen U<VAR>h2U : U.Nonempty<GOAL>0 < μ.outerMeasure U
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>μ : MeasureTheory.Content G<VAR>R1Space G<VAR>S : MeasurableSpace G<VAR>BorelSpace G<GOAL>S ≤ μ.outerMeasure.caratheodory
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>μ : MeasureTheory.Content G<VAR>R1Space G<VAR>S : MeasurableSpace G<VAR>BorelSpace G<VAR>s : Set G<VAR>hs : MeasurableSet s<GOAL>μ.measure s = μ.outerMeasure s
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>μ : MeasureTheory.Content G<VAR>H : μ.ContentRegular<VAR>K : TopologicalSpace.Compacts G<VAR>ε : ℝ≥0<VAR>hε : ε ≠ 0<GOAL>∃ K', K.carrier ⊆ interior K'.carrier ∧ (fun s => ↑(μ.toFun s)) K' ≤ (fun s => ↑(μ.toFun s)) K + ↑ε
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>μ : MeasureTheory.Content G<VAR>MeasurableSpace G<VAR>R1Space G<VAR>BorelSpace G<VAR>H : μ.ContentRegular<VAR>K : TopologicalSpace.Compacts G<GOAL>μ.measure ↑K = (fun s => ↑(μ.toFun s)) K
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : α → E<VAR>hf : MeasureTheory.Integrable f μ<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>↑(μ.withDensityᵥ f) s = ∫ (x : α) in s, f x ∂μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<GOAL>μ.withDensityᵥ 0 = 0
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : α → E<GOAL>μ.withDensityᵥ (-f) = -μ.withDensityᵥ f
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : α → E<GOAL>(μ.withDensityᵥ fun x => -f x) = -μ.withDensityᵥ f
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f g : α → E<VAR>hf : MeasureTheory.Integrable f μ<VAR>hg : MeasureTheory.Integrable g μ<GOAL>μ.withDensityᵥ (f + g) = μ.withDensityᵥ f + μ.withDensityᵥ g
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f g : α → E<VAR>hf : MeasureTheory.Integrable f μ<VAR>hg : MeasureTheory.Integrable g μ<GOAL>(μ.withDensityᵥ fun x => f x + g x) = μ.withDensityᵥ f + μ.withDensityᵥ g
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f g : α → E<VAR>hf : MeasureTheory.Integrable f μ<VAR>hg : MeasureTheory.Integrable g μ<GOAL>μ.withDensityᵥ (f - g) = μ.withDensityᵥ f - μ.withDensityᵥ g
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f g : α → E<VAR>hf : MeasureTheory.Integrable f μ<VAR>hg : MeasureTheory.Integrable g μ<GOAL>(μ.withDensityᵥ fun x => f x - g x) = μ.withDensityᵥ f - μ.withDensityᵥ g
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>𝕜 : Type u_4<VAR>NontriviallyNormedField 𝕜<VAR>NormedSpace 𝕜 E<VAR>SMulCommClass ℝ 𝕜 E<VAR>f : α → E<VAR>r : 𝕜<GOAL>μ.withDensityᵥ (r • f) = r • μ.withDensityᵥ f
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>𝕜 : Type u_4<VAR>NontriviallyNormedField 𝕜<VAR>NormedSpace 𝕜 E<VAR>SMulCommClass ℝ 𝕜 E<VAR>f : α → E<VAR>r : 𝕜<GOAL>(μ.withDensityᵥ fun x => r • f x) = r • μ.withDensityᵥ f
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : α → ℝ≥0<VAR>g : α → E<VAR>hf : AEMeasurable f μ<VAR>hfg : MeasureTheory.Integrable (f • g) μ<GOAL>μ.withDensityᵥ (f • g) = (μ.withDensity fun x => ↑(f x)).withDensityᵥ g
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : α → ℝ≥0∞<VAR>g : α → E<VAR>hf : AEMeasurable f μ<VAR>hflt : ∀ᵐ (x : α) ∂μ, f x < ⊤<VAR>hfg : MeasureTheory.Integrable (fun x => (f x).toReal • g x) μ<GOAL>(μ.withDensityᵥ fun x => (f x).toReal • g x) = (μ.withDensity f).withDensityᵥ g
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ<GOAL>μ.withDensityᵥ f ≪ᵥ μ.toENNRealVectorMeasure
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f g : α → E<VAR>hf : MeasureTheory.Integrable f μ<VAR>hg : MeasureTheory.Integrable g μ<VAR>hfg : μ.withDensityᵥ f = μ.withDensityᵥ g<GOAL>f =ᵐ[μ] g
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f g : α → E<VAR>h : f =ᵐ[μ] g<GOAL>μ.withDensityᵥ f = μ.withDensityᵥ g
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f g : α → E<VAR>hf : MeasureTheory.Integrable f μ<VAR>hg : MeasureTheory.Integrable g μ<GOAL>μ.withDensityᵥ f = μ.withDensityᵥ g ↔ f =ᵐ[μ] g
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<VAR>hfm : AEMeasurable f μ<VAR>hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤<GOAL>(μ.withDensityᵥ fun x => (f x).toReal) = (μ.withDensity f).toSignedMeasure
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ<VAR>hfi : MeasureTheory.Integrable f μ<GOAL>μ.withDensityᵥ f = (μ.withDensity fun x => ENNReal.ofReal (f x)).toSignedMeasure - (μ.withDensity fun x => ENNReal.ofReal (-f x)).toSignedMeasure
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>hm : m ≤ m0<VAR>f : α → ℝ<VAR>hf : MeasureTheory.Integrable f μ<VAR>i : Set α<VAR>hi : MeasurableSet i<GOAL>↑((μ.withDensityᵥ f).trim hm) i = ∫ (x : α) in i, f x ∂μ
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : α → E<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>hm : m ≤ m0<VAR>hfi : MeasureTheory.Integrable f μ<GOAL>(μ.withDensityᵥ f).trim hm ≪ᵥ (μ.trim hm).toENNRealVectorMeasure
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>β : Type u_2<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.FiniteMeasure α<VAR>ν : MeasureTheory.FiniteMeasure β<GOAL>↑(μ.prod ν) = (↑μ).prod ↑ν
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>β : Type u_2<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.FiniteMeasure α<VAR>ν : MeasureTheory.FiniteMeasure β<VAR>s : Set (α × β)<VAR>s_mble : MeasurableSet s<GOAL>(μ.prod ν) s = (∫⁻ (x : α), ↑ν (Prod.mk x ⁻¹' s) ∂↑μ).toNNReal
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>β : Type u_2<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.FiniteMeasure α<VAR>ν : MeasureTheory.FiniteMeasure β<VAR>s : Set (α × β)<VAR>s_mble : MeasurableSet s<GOAL>(μ.prod ν) s = (∫⁻ (y : β), ↑μ ((fun x => (x, y)) ⁻¹' s) ∂↑ν).toNNReal
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>β : Type u_2<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.FiniteMeasure α<VAR>ν : MeasureTheory.FiniteMeasure β<VAR>s : Set α<VAR>t : Set β<GOAL>(μ.prod ν) (s ×ˢ t) = μ s * ν t
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>β : Type u_2<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.FiniteMeasure α<VAR>ν : MeasureTheory.FiniteMeasure β<GOAL>(μ.prod ν).mass = μ.mass * ν.mass
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>β : Type u_2<VAR>MeasurableSpace β<VAR>ν : MeasureTheory.FiniteMeasure β<GOAL>MeasureTheory.FiniteMeasure.prod 0 ν = 0
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>β : Type u_2<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.FiniteMeasure α<GOAL>μ.prod 0 = 0
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>β : Type u_2<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.FiniteMeasure α<VAR>ν : MeasureTheory.FiniteMeasure β<GOAL>(μ.prod ν).map Prod.fst = ν Set.univ • μ
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>β : Type u_2<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.FiniteMeasure α<VAR>ν : MeasureTheory.FiniteMeasure β<GOAL>(μ.prod ν).map Prod.snd = μ Set.univ • ν
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>β : Type u_2<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.FiniteMeasure α<VAR>ν : MeasureTheory.FiniteMeasure β<VAR>α' : Type u_3<VAR>MeasurableSpace α'<VAR>β' : Type u_4<VAR>MeasurableSpace β'<VAR>f : α → α'<VAR>g : β → β'<VAR>f_mble : Measurable f<VAR>g_mble : Measurable g<GOAL>(μ.map f).prod (ν.map g) = (μ.prod ν).map (Prod.map f g)