ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>OpensMeasurableSpace α<VAR>μ.InnerRegular<VAR>hs : MeasurableSet s<GOAL>μ.everywherePosSubset s =ᵐ[μ] s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>OpensMeasurableSpace α<VAR>μ.InnerRegularCompactLTTop<VAR>hs : MeasurableSet s<VAR>h's : μ s ≠ ⊤<GOAL>μ.everywherePosSubset s =ᵐ[μ] s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>OpensMeasurableSpace α<VAR>μ.InnerRegular<VAR>hs : MeasurableSet s<GOAL>μ.IsEverywherePos (μ.everywherePosSubset s)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>OpensMeasurableSpace α<VAR>μ.InnerRegularCompactLTTop<VAR>hs : MeasurableSet s<VAR>h's : μ s ≠ ⊤<GOAL>μ.IsEverywherePos (μ.everywherePosSubset s)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>hs : μ.IsEverywherePos s<VAR>c : ℝ≥0∞<VAR>hc : c ≠ 0<GOAL>(c • μ).IsEverywherePos s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>hs : μ.IsEverywherePos s<VAR>c : ℝ≥0<VAR>hc : c ≠ 0<GOAL>(c • μ).IsEverywherePos s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>s : Set α<VAR>hs : μ.IsEverywherePos s<VAR>h : ∀ x ∈ s, ∃ t ∈ 𝓝 x, ∀ u ⊆ t, ν u = μ u<GOAL>ν.IsEverywherePos s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>s : Set α<VAR>h : ∀ x ∈ s, ∃ t ∈ 𝓝 x, ∀ u ⊆ t, ν u = μ u<GOAL>ν.IsEverywherePos s ↔ μ.IsEverywherePos s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>μ.IsOpenPosMeasure<VAR>hs : IsOpen s<GOAL>μ.IsEverywherePos s
<VAR>G : Type u_2<VAR>Group G<VAR>TopologicalSpace G<VAR>TopologicalGroup G<VAR>LocallyCompactSpace G<VAR>MeasurableSpace G<VAR>BorelSpace G<VAR>μ : MeasureTheory.Measure G<VAR>μ.IsMulLeftInvariant<VAR>MeasureTheory.IsFiniteMeasureOnCompacts μ<VAR>μ.InnerRegularCompactLTTop<VAR>k : Set G<VAR>h : μ.IsEverywherePos k<VAR>hk : IsCompact k<VAR>h'k : IsClosed k<GOAL>IsGδ k
<VAR>G : Type u_2<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>LocallyCompactSpace G<VAR>MeasurableSpace G<VAR>BorelSpace G<VAR>μ : MeasureTheory.Measure G<VAR>μ.IsAddLeftInvariant<VAR>MeasureTheory.IsFiniteMeasureOnCompacts μ<VAR>μ.InnerRegularCompactLTTop<VAR>k : Set G<VAR>h : μ.IsEverywherePos k<VAR>hk : IsCompact k<VAR>h'k : IsClosed k<GOAL>IsGδ k
<VAR>G : Type u_2<VAR>Group G<VAR>TopologicalSpace G<VAR>TopologicalGroup G<VAR>LocallyCompactSpace G<VAR>MeasurableSpace G<VAR>BorelSpace G<VAR>μ : MeasureTheory.Measure G<VAR>μ.IsMulLeftInvariant<VAR>MeasureTheory.IsFiniteMeasureOnCompacts μ<VAR>μ.InnerRegularCompactLTTop<GOAL>μ.InnerRegularWRT (fun s => ∃ f, Continuous f ∧ HasCompactSupport f ∧ s = f ⁻¹' {1}) fun s => MeasurableSet s ∧ μ s ≠ ⊤
<VAR>G : Type u_2<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>LocallyCompactSpace G<VAR>MeasurableSpace G<VAR>BorelSpace G<VAR>μ : MeasureTheory.Measure G<VAR>μ.IsAddLeftInvariant<VAR>MeasureTheory.IsFiniteMeasureOnCompacts μ<VAR>μ.InnerRegularCompactLTTop<GOAL>μ.InnerRegularWRT (fun s => ∃ f, Continuous f ∧ HasCompactSupport f ∧ s = f ⁻¹' {1}) fun s => MeasurableSet s ∧ μ s ≠ ⊤
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>CompleteSpace 𝕜<VAR>NormedAddCommGroup E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>MeasurableSpace F<VAR>BorelSpace F<VAR>NormedSpace 𝕜 F<VAR>L : E →ₗ[𝕜] F<VAR>μ : MeasureTheory.Measure E<VAR>ν : MeasureTheory.Measure F<VAR>μ.IsAddHaarMeasure<VAR>ν.IsAddHaarMeasure<VAR>LocallyCompactSpace E<VAR>h : Function.Surjective ⇑L<GOAL>∃ c, 0 < c ∧ c < ⊤ ∧ MeasureTheory.Measure.map (⇑L) μ = (c * MeasureTheory.Measure.addHaar Set.univ) • ν
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>CompleteSpace 𝕜<VAR>NormedAddCommGroup E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>MeasurableSpace F<VAR>BorelSpace F<VAR>NormedSpace 𝕜 F<VAR>L : E →ₗ[𝕜] F<VAR>μ : MeasureTheory.Measure E<VAR>ν : MeasureTheory.Measure F<VAR>μ.IsAddHaarMeasure<VAR>ν.IsAddHaarMeasure<VAR>LocallyCompactSpace E<VAR>h : Function.Surjective ⇑L<GOAL>∃ c, 0 < c ∧ MeasureTheory.Measure.map (⇑L) μ = c • ν
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>CompleteSpace 𝕜<VAR>NormedAddCommGroup E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>MeasurableSpace F<VAR>BorelSpace F<VAR>NormedSpace 𝕜 F<VAR>L : E →ₗ[𝕜] F<VAR>μ : MeasureTheory.Measure E<VAR>ν : MeasureTheory.Measure F<VAR>μ.IsAddHaarMeasure<VAR>ν.IsAddHaarMeasure<VAR>LocallyCompactSpace E<VAR>h : Function.Surjective ⇑L<VAR>s : Set F<VAR>hs : MeasurableSet s<GOAL>(∀ᵐ (x : E) ∂μ, L x ∈ s) ↔ ∀ᵐ (y : F) ∂ν, y ∈ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>CompleteSpace 𝕜<VAR>NormedAddCommGroup E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>MeasurableSpace F<VAR>BorelSpace F<VAR>NormedSpace 𝕜 F<VAR>L : E →ₗ[𝕜] F<VAR>μ : MeasureTheory.Measure E<VAR>ν : MeasureTheory.Measure F<VAR>μ.IsAddHaarMeasure<VAR>ν.IsAddHaarMeasure<VAR>LocallyCompactSpace E<VAR>LocallyCompactSpace F<VAR>s : Set F<VAR>hs : MeasurableSet s<GOAL>(∀ᵐ (y : F) ∂ν, ∀ᵐ (x : E) ∂μ, y + L x ∈ s) ↔ ∀ᵐ (y : F) ∂ν, y ∈ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>CompleteSpace 𝕜<VAR>NormedAddCommGroup E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>MeasurableSpace F<VAR>BorelSpace F<VAR>NormedSpace 𝕜 F<VAR>L : E →ₗ[𝕜] F<VAR>μ : MeasureTheory.Measure E<VAR>ν : MeasureTheory.Measure F<VAR>μ.IsAddHaarMeasure<VAR>ν.IsAddHaarMeasure<VAR>LocallyCompactSpace E<VAR>LocallyCompactSpace F<VAR>s : Set F<VAR>hs : MeasurableSet s<VAR>h : ∀ (y : F), ∀ᵐ (x : E) ∂μ, y + L x ∈ s<GOAL>∀ᵐ (y : F) ∂ν, y ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>f g : α → β<VAR>hf : MeasureTheory.AEStronglyMeasurable' m f μ<VAR>hfg : f =ᵐ[μ] g<GOAL>MeasureTheory.AEStronglyMeasurable' m g μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>m' : MeasurableSpace α<VAR>hf : MeasureTheory.AEStronglyMeasurable' m f μ<VAR>hm : m ≤ m'<GOAL>MeasureTheory.AEStronglyMeasurable' m' f μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>f g : α → β<VAR>Add β<VAR>ContinuousAdd β<VAR>hf : MeasureTheory.AEStronglyMeasurable' m f μ<VAR>hg : MeasureTheory.AEStronglyMeasurable' m g μ<GOAL>MeasureTheory.AEStronglyMeasurable' m (f + g) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>AddGroup β<VAR>TopologicalAddGroup β<VAR>f : α → β<VAR>hfm : MeasureTheory.AEStronglyMeasurable' m f μ<GOAL>MeasureTheory.AEStronglyMeasurable' m (-f) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>AddGroup β<VAR>TopologicalAddGroup β<VAR>f g : α → β<VAR>hfm : MeasureTheory.AEStronglyMeasurable' m f μ<VAR>hgm : MeasureTheory.AEStronglyMeasurable' m g μ<GOAL>MeasureTheory.AEStronglyMeasurable' m (f - g) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝕜 : Type u_3<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>SMul 𝕜 β<VAR>ContinuousConstSMul 𝕜 β<VAR>c : 𝕜<VAR>hf : MeasureTheory.AEStronglyMeasurable' m f μ<GOAL>MeasureTheory.AEStronglyMeasurable' m (c • f) μ
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>𝕜 : Type u_4<VAR>β : Type u_5<VAR>RCLike 𝕜<VAR>NormedAddCommGroup β<VAR>InnerProductSpace 𝕜 β<VAR>f : α → β<VAR>hfm : MeasureTheory.AEStronglyMeasurable' m f μ<VAR>c : β<GOAL>MeasureTheory.AEStronglyMeasurable' m (fun x => ⟪c, f x⟫_𝕜) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>hfm : MeasureTheory.AEStronglyMeasurable' m f μ<GOAL>MeasureTheory.StronglyMeasurable (MeasureTheory.AEStronglyMeasurable'.mk f hfm)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>hfm : MeasureTheory.AEStronglyMeasurable' m f μ<GOAL>f =ᵐ[μ] MeasureTheory.AEStronglyMeasurable'.mk f hfm
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>γ : Type u_4<VAR>TopologicalSpace γ<VAR>f : α → β<VAR>g : β → γ<VAR>hg : Continuous g<VAR>hf : MeasureTheory.AEStronglyMeasurable' m f μ<GOAL>MeasureTheory.AEStronglyMeasurable' m (g ∘ f) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m m0 m0' : MeasurableSpace α<VAR>TopologicalSpace β<VAR>hm0 : m0 ≤ m0'<VAR>μ : MeasureTheory.Measure α<VAR>f : α → β<VAR>hf : MeasureTheory.AEStronglyMeasurable' m f (μ.trim hm0)<GOAL>MeasureTheory.AEStronglyMeasurable' m f μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<GOAL>∀ {x : MeasurableSpace α} [inst : TopologicalSpace β] {μ : MeasureTheory.Measure α} {f : α → β}, MeasureTheory.StronglyMeasurable f → MeasureTheory.AEStronglyMeasurable' m f μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace β<VAR>TopologicalSpace.MetrizableSpace β<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → β<VAR>hm : m ≤ m0<VAR>hfm : MeasureTheory.AEStronglyMeasurable' m f μ<VAR>hgm : MeasureTheory.AEStronglyMeasurable' m g μ<GOAL>MeasureTheory.AEStronglyMeasurable'.mk f hfm =ᵐ[μ.trim hm] MeasureTheory.AEStronglyMeasurable'.mk g hgm ↔ f =ᵐ[μ] g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>TopologicalSpace β<VAR>mα : MeasurableSpace α<GOAL>∀ {x : MeasurableSpace γ} {f : α → β} {μ : MeasureTheory.Measure γ} {g : γ → α}, MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.map g μ) → AEMeasurable g μ → MeasureTheory.AEStronglyMeasurable' (MeasurableSpace.comap g mα) (f ∘ g) μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m₂ m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace E<VAR>Zero E<VAR>hm : m ≤ m0<VAR>s : Set α<VAR>f : α → E<VAR>hs_m : MeasurableSet s<VAR>hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)<VAR>hf : MeasureTheory.AEStronglyMeasurable' m f μ<VAR>hf_zero : f =ᵐ[μ.restrict sᶜ] 0<GOAL>MeasureTheory.AEStronglyMeasurable' m₂ f μ
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>p : ℝ≥0∞<VAR>NormedAddCommGroup F<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : ↥(MeasureTheory.Lp F p μ)<GOAL>f ∈ MeasureTheory.lpMeasSubgroup F m p μ ↔ MeasureTheory.AEStronglyMeasurable' m (↑↑f) μ
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>𝕜 : Type u_5<VAR>p : ℝ≥0∞<VAR>RCLike 𝕜<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : ↥(MeasureTheory.Lp F p μ)<GOAL>f ∈ MeasureTheory.lpMeas F 𝕜 m p μ ↔ MeasureTheory.AEStronglyMeasurable' m (↑↑f) μ
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>𝕜 : Type u_5<VAR>p : ℝ≥0∞<VAR>RCLike 𝕜<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>m : MeasurableSpace α<GOAL>∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : ↥(MeasureTheory.lpMeas F 𝕜 m p μ)), MeasureTheory.AEStronglyMeasurable' m (↑↑↑f) μ
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>𝕜 : Type u_5<VAR>p : ℝ≥0∞<VAR>RCLike 𝕜<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : ↥(MeasureTheory.Lp F p μ)<GOAL>f ∈ MeasureTheory.lpMeas F 𝕜 m0 p μ
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>p : ℝ≥0∞<VAR>NormedAddCommGroup F<VAR>m : MeasurableSpace α<GOAL>∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : ↥(MeasureTheory.lpMeasSubgroup F m p μ)}, ↑↑↑f = ↑↑↑f
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>𝕜 : Type u_5<VAR>p : ℝ≥0∞<VAR>RCLike 𝕜<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>m : MeasurableSpace α<GOAL>∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : ↥(MeasureTheory.lpMeas F 𝕜 m p μ)}, ↑↑↑f = ↑↑↑f
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>𝕜 : Type u_5<VAR>p : ℝ≥0∞<VAR>RCLike 𝕜<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>m m0 : MeasurableSpace α<VAR>hm : m ≤ m0<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>c : F<GOAL>MeasureTheory.indicatorConstLp p ⋯ hμs c ∈ MeasureTheory.lpMeas F 𝕜 m p μ
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>p : ℝ≥0∞<VAR>NormedAddCommGroup F<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>hm : m ≤ m0<VAR>f : ↥(MeasureTheory.Lp F p μ)<VAR>hf_meas : f ∈ MeasureTheory.lpMeasSubgroup F m p μ<GOAL>MeasureTheory.Memℒp (Exists.choose ⋯) p (μ.trim hm)
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>p : ℝ≥0∞<VAR>NormedAddCommGroup F<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>hm : m ≤ m0<VAR>f : ↥(MeasureTheory.Lp F p (μ.trim hm))<GOAL>MeasureTheory.Memℒp.toLp ↑↑f ⋯ ∈ MeasureTheory.lpMeasSubgroup F m p μ
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>p : ℝ≥0∞<VAR>NormedAddCommGroup F<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>hm : m ≤ m0<VAR>f : ↥(MeasureTheory.lpMeasSubgroup F m p μ)<GOAL>↑↑(MeasureTheory.lpMeasSubgroupToLpTrim F p μ hm f) =ᵐ[μ] ↑↑↑f
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>p : ℝ≥0∞<VAR>NormedAddCommGroup F<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>hm : m ≤ m0<VAR>f : ↥(MeasureTheory.Lp F p (μ.trim hm))<GOAL>↑↑↑(MeasureTheory.lpTrimToLpMeasSubgroup F p μ hm f) =ᵐ[μ] ↑↑f
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>𝕜 : Type u_5<VAR>p : ℝ≥0∞<VAR>RCLike 𝕜<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>hm : m ≤ m0<VAR>f : ↥(MeasureTheory.lpMeas F 𝕜 m p μ)<GOAL>↑↑(MeasureTheory.lpMeasToLpTrim F 𝕜 p μ hm f) =ᵐ[μ] ↑↑↑f
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>𝕜 : Type u_5<VAR>p : ℝ≥0∞<VAR>RCLike 𝕜<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>hm : m ≤ m0<VAR>f : ↥(MeasureTheory.Lp F p (μ.trim hm))<GOAL>↑↑↑(MeasureTheory.lpTrimToLpMeas F 𝕜 p μ hm f) =ᵐ[μ] ↑↑f
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>p : ℝ≥0∞<VAR>NormedAddCommGroup F<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>hm : m ≤ m0<GOAL>Function.RightInverse (MeasureTheory.lpTrimToLpMeasSubgroup F p μ hm) (MeasureTheory.lpMeasSubgroupToLpTrim F p μ hm)
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>p : ℝ≥0∞<VAR>NormedAddCommGroup F<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>hm : m ≤ m0<GOAL>Function.LeftInverse (MeasureTheory.lpTrimToLpMeasSubgroup F p μ hm) (MeasureTheory.lpMeasSubgroupToLpTrim F p μ hm)
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>p : ℝ≥0∞<VAR>NormedAddCommGroup F<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>hm : m ≤ m0<VAR>f g : ↥(MeasureTheory.lpMeasSubgroup F m p μ)<GOAL>MeasureTheory.lpMeasSubgroupToLpTrim F p μ hm (f + g) = MeasureTheory.lpMeasSubgroupToLpTrim F p μ hm f + MeasureTheory.lpMeasSubgroupToLpTrim F p μ hm g
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>p : ℝ≥0∞<VAR>NormedAddCommGroup F<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>hm : m ≤ m0<VAR>f : ↥(MeasureTheory.lpMeasSubgroup F m p μ)<GOAL>MeasureTheory.lpMeasSubgroupToLpTrim F p μ hm (-f) = -MeasureTheory.lpMeasSubgroupToLpTrim F p μ hm f
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>p : ℝ≥0∞<VAR>NormedAddCommGroup F<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>hm : m ≤ m0<VAR>f g : ↥(MeasureTheory.lpMeasSubgroup F m p μ)<GOAL>MeasureTheory.lpMeasSubgroupToLpTrim F p μ hm (f - g) = MeasureTheory.lpMeasSubgroupToLpTrim F p μ hm f - MeasureTheory.lpMeasSubgroupToLpTrim F p μ hm g
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>𝕜 : Type u_5<VAR>p : ℝ≥0∞<VAR>RCLike 𝕜<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>hm : m ≤ m0<VAR>c : 𝕜<VAR>f : ↥(MeasureTheory.lpMeas F 𝕜 m p μ)<GOAL>MeasureTheory.lpMeasToLpTrim F 𝕜 p μ hm (c • f) = c • MeasureTheory.lpMeasToLpTrim F 𝕜 p μ hm f
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>p : ℝ≥0∞<VAR>NormedAddCommGroup F<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>hp : Fact (1 ≤ p)<VAR>hm : m ≤ m0<VAR>f : ↥(MeasureTheory.lpMeasSubgroup F m p μ)<GOAL>‖MeasureTheory.lpMeasSubgroupToLpTrim F p μ hm f‖ = ‖f‖
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>p : ℝ≥0∞<VAR>NormedAddCommGroup F<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>hp : Fact (1 ≤ p)<VAR>hm : m ≤ m0<GOAL>Isometry (MeasureTheory.lpMeasSubgroupToLpTrim F p μ hm)
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>p : ℝ≥0∞<VAR>NormedAddCommGroup F<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>hp : Fact (1 ≤ p)<VAR>CompleteSpace F<VAR>hm : m ≤ m0<GOAL>IsComplete {f | MeasureTheory.AEStronglyMeasurable' m (↑↑f) μ}
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>p : ℝ≥0∞<VAR>NormedAddCommGroup F<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>Fact (1 ≤ p)<VAR>CompleteSpace F<VAR>hm : m ≤ m0<GOAL>IsClosed {f | MeasureTheory.AEStronglyMeasurable' m (↑↑f) μ}
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>𝕜 : Type u_5<VAR>p : ℝ≥0∞<VAR>RCLike 𝕜<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>hm : m ≤ m0<VAR>f : ↥(MeasureTheory.lpMeas F 𝕜 m p μ)<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<GOAL>∃ g, MeasureTheory.FinStronglyMeasurable g (μ.trim hm) ∧ ↑↑↑f =ᵐ[μ] g
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>p : ℝ≥0∞<VAR>NormedAddCommGroup F<VAR>m m0 : MeasurableSpace α<VAR>one_le_p : Fact (1 ≤ p)<VAR>NormedSpace ℝ F<VAR>hm : m ≤ m0<VAR>s : Set α<VAR>μ : MeasureTheory.Measure α<VAR>hs : MeasurableSet s<VAR>hμs : (μ.trim hm) s ≠ ⊤<VAR>c : F<GOAL>↑((MeasureTheory.lpMeasToLpTrimLie F ℝ p μ hm).symm (MeasureTheory.indicatorConstLp p hs hμs c)) = MeasureTheory.indicatorConstLp p ⋯ ⋯ c
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>p : ℝ≥0∞<VAR>NormedAddCommGroup F<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>one_le_p : Fact (1 ≤ p)<VAR>NormedSpace ℝ F<VAR>hm : m ≤ m0<VAR>f : α → F<VAR>hf : MeasureTheory.Memℒp f p (μ.trim hm)<GOAL>↑((MeasureTheory.lpMeasToLpTrimLie F ℝ p μ hm).symm (MeasureTheory.Memℒp.toLp f hf)) = MeasureTheory.Memℒp.toLp f ⋯
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>p : ℝ≥0∞<VAR>NormedAddCommGroup F<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>Fact (1 ≤ p)<VAR>NormedSpace ℝ F<VAR>hm : m ≤ m0<VAR>hp_ne_top : p ≠ ⊤<VAR>P : ↥(MeasureTheory.Lp F p μ) → Prop<VAR>h_ind : ∀ (c : F) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ⊤), P ↑(MeasureTheory.Lp.simpleFunc.indicatorConst p ⋯ ⋯ c)<VAR>h_add : ∀ ⦃f g : α → F⦄ (hf : MeasureTheory.Memℒp f p μ) (hg : MeasureTheory.Memℒp g p μ), MeasureTheory.AEStronglyMeasurable' m f μ → MeasureTheory.AEStronglyMeasurable' m g μ → Disjoint (Function.support f) (Function.support g) → P (MeasureTheory.Memℒp.toLp f hf) → P (MeasureTheory.Memℒp.toLp g hg) → P (MeasureTheory.Memℒp.toLp f hf + MeasureTheory.Memℒp.toLp g hg)<VAR>h_closed : IsClosed {f | P ↑f}<VAR>f : ↥(MeasureTheory.Lp F p μ)<GOAL>MeasureTheory.AEStronglyMeasurable' m (↑↑f) μ → P f
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>p : ℝ≥0∞<VAR>NormedAddCommGroup F<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>Fact (1 ≤ p)<VAR>NormedSpace ℝ F<VAR>hm : m ≤ m0<VAR>hp_ne_top : p ≠ ⊤<VAR>P : ↥(MeasureTheory.Lp F p μ) → Prop<VAR>h_ind : ∀ (c : F) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ⊤), P ↑(MeasureTheory.Lp.simpleFunc.indicatorConst p ⋯ ⋯ c)<VAR>h_add : ∀ ⦃f g : α → F⦄ (hf : MeasureTheory.Memℒp f p μ) (hg : MeasureTheory.Memℒp g p μ), MeasureTheory.StronglyMeasurable f → MeasureTheory.StronglyMeasurable g → Disjoint (Function.support f) (Function.support g) → P (MeasureTheory.Memℒp.toLp f hf) → P (MeasureTheory.Memℒp.toLp g hg) → P (MeasureTheory.Memℒp.toLp f hf + MeasureTheory.Memℒp.toLp g hg)<VAR>h_closed : IsClosed {f | P ↑f}<VAR>f : ↥(MeasureTheory.Lp F p μ)<GOAL>MeasureTheory.AEStronglyMeasurable' m (↑↑f) μ → P f
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>p : ℝ≥0∞<VAR>NormedAddCommGroup F<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>Fact (1 ≤ p)<VAR>NormedSpace ℝ F<VAR>hm : m ≤ m0<VAR>hp_ne_top : p ≠ ⊤<VAR>P : (α → F) → Prop<VAR>h_ind : ∀ (c : F) ⦃s : Set α⦄, MeasurableSet s → μ s < ⊤ → P (s.indicator fun x => c)<VAR>h_add : ∀ ⦃f g : α → F⦄, Disjoint (Function.support f) (Function.support g) → MeasureTheory.Memℒp f p μ → MeasureTheory.Memℒp g p μ → MeasureTheory.StronglyMeasurable f → MeasureTheory.StronglyMeasurable g → P f → P g → P (f + g)<VAR>h_closed : IsClosed {f | P ↑↑↑f}<VAR>h_ae : ∀ ⦃f g : α → F⦄, f =ᵐ[μ] g → MeasureTheory.Memℒp f p μ → P f → P g<VAR>f : α → F<GOAL>MeasureTheory.Memℒp f p μ → MeasureTheory.AEStronglyMeasurable' m f μ → P f
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → ℝ<VAR>s : Set α<VAR>MeasureTheory.SigmaFinite μ<VAR>f_int : MeasureTheory.IntegrableOn f s μ<VAR>g_int : MeasureTheory.IntegrableOn g s μ<VAR>hs : MeasurableSet s<VAR>hfg : f ≤ᵐ[μ.restrict s] g<GOAL>(μ.prod MeasureTheory.volume) (regionBetween f g s) = ENNReal.ofReal (∫ (y : α) in s, (g - f) y ∂μ)
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → ℝ<VAR>s : Set α<VAR>MeasureTheory.SigmaFinite μ<VAR>f_int : MeasureTheory.IntegrableOn f s μ<VAR>g_int : MeasureTheory.IntegrableOn g s μ<VAR>hs : MeasurableSet s<VAR>hfg : ∀ x ∈ s, f x ≤ g x<GOAL>(μ.prod MeasureTheory.volume) (regionBetween f g s) = ENNReal.ofReal (∫ (y : α) in s, (g - f) y ∂μ)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>f : C(ℝ, E)<VAR>hf : Summable fun n => ‖ContinuousMap.restrict (Set.Icc 0 1) (f.comp (ContinuousMap.addRight ↑n))‖<GOAL>MeasureTheory.Integrable (⇑f) MeasureTheory.volume
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>c : ℝ<VAR>f : ℝ → E<GOAL>∫ (x : ℝ) in Set.Iic c, f (-x) = ∫ (x : ℝ) in Set.Ioi (-c), f x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>c : ℝ<VAR>f : ℝ → E<GOAL>∫ (x : ℝ) in Set.Ioi c, f (-x) = ∫ (x : ℝ) in Set.Iic (-c), f x
<VAR>f : ℝ → ℝ<GOAL>∫ (x : ℝ), f |x| = 2 * ∫ (x : ℝ) in Set.Ioi 0, f x
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>ι : Type u_2<VAR>L : Filter ι<VAR>μ : MeasureTheory.Measure Ω<VAR>μs : ι → MeasureTheory.Measure Ω<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μs i)<VAR>E : Set Ω<VAR>E_mble : MeasurableSet E<VAR>h : Filter.limsup (fun i => (μs i) E) L ≤ μ E<GOAL>μ Eᶜ ≤ Filter.liminf (fun i => (μs i) Eᶜ) L
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>ι : Type u_2<VAR>L : Filter ι<VAR>μ : MeasureTheory.Measure Ω<VAR>μs : ι → MeasureTheory.Measure Ω<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μs i)<VAR>E : Set Ω<VAR>E_mble : MeasurableSet E<VAR>h : Filter.limsup (fun i => (μs i) Eᶜ) L ≤ μ Eᶜ<GOAL>μ E ≤ Filter.liminf (fun i => (μs i) E) L
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>ι : Type u_2<VAR>L : Filter ι<VAR>μ : MeasureTheory.Measure Ω<VAR>μs : ι → MeasureTheory.Measure Ω<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μs i)<VAR>E : Set Ω<VAR>E_mble : MeasurableSet E<VAR>h : μ E ≤ Filter.liminf (fun i => (μs i) E) L<GOAL>Filter.limsup (fun i => (μs i) Eᶜ) L ≤ μ Eᶜ
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>ι : Type u_2<VAR>L : Filter ι<VAR>μ : MeasureTheory.Measure Ω<VAR>μs : ι → MeasureTheory.Measure Ω<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μs i)<VAR>E : Set Ω<VAR>E_mble : MeasurableSet E<VAR>h : μ Eᶜ ≤ Filter.liminf (fun i => (μs i) Eᶜ) L<GOAL>Filter.limsup (fun i => (μs i) E) L ≤ μ E
<VAR>Ω : Type u_1<VAR>MeasurableSpace Ω<VAR>TopologicalSpace Ω<VAR>OpensMeasurableSpace Ω<VAR>ι : Type u_2<VAR>L : Filter ι<VAR>μ : MeasureTheory.Measure Ω<VAR>μs : ι → MeasureTheory.Measure Ω<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μs i)<GOAL>(∀ (F : Set Ω), IsClosed F → Filter.limsup (fun i => (μs i) F) L ≤ μ F) ↔ ∀ (G : Set Ω), IsOpen G → μ G ≤ Filter.liminf (fun i => (μs i) G) L