ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>s : Finset E<VAR>hs : ∀ c ∈ s, ‖c‖ ≤ 2<VAR>h : ∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 ≤ ‖c - d‖<GOAL>s.card ≤ 5 ^ FiniteDimensional.finrank ℝ E
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<GOAL>Besicovitch.multiplicity E ≤ 5 ^ FiniteDimensional.finrank ℝ E
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>s : Finset E<VAR>hs : ∀ c ∈ s, ‖c‖ ≤ 2<VAR>h's : ∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 ≤ ‖c - d‖<GOAL>s.card ≤ Besicovitch.multiplicity E
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<GOAL>∃ δ, 0 < δ ∧ δ < 1 ∧ ∀ (s : Finset E), (∀ c ∈ s, ‖c‖ ≤ 2) → (∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 - δ ≤ ‖c - d‖) → s.card ≤ Besicovitch.multiplicity E
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<GOAL>Besicovitch.goodδ E < 1
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<GOAL>1 < Besicovitch.goodτ E
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>s : Finset E<VAR>hs : ∀ c ∈ s, ‖c‖ ≤ 2<VAR>h's : ∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 - Besicovitch.goodδ E ≤ ‖c - d‖<GOAL>s.card ≤ Besicovitch.multiplicity E
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>n : ℕ<VAR>f : Fin n → E<VAR>h : ∀ (i : Fin n), ‖f i‖ ≤ 2<VAR>h' : Pairwise fun i j => 1 - Besicovitch.goodδ E ≤ ‖f i - f j‖<GOAL>n ≤ Besicovitch.multiplicity E
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>N : ℕ<VAR>τ : ℝ<VAR>a : Besicovitch.SatelliteConfig E N τ<VAR>lastr : a.r (Fin.last N) = 1<VAR>hτ : 1 ≤ τ<VAR>δ : ℝ<VAR>hδ1 : τ ≤ 1 + δ / 4<VAR>hδ2 : δ ≤ 1<VAR>i j : Fin N.succ<VAR>inej : i ≠ j<GOAL>1 - δ ≤ ‖a.c i - a.c j‖
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>N : ℕ<VAR>τ : ℝ<VAR>a : Besicovitch.SatelliteConfig E N τ<VAR>lastc : a.c (Fin.last N) = 0<VAR>lastr : a.r (Fin.last N) = 1<VAR>hτ : 1 ≤ τ<VAR>δ : ℝ<VAR>hδ1 : τ ≤ 1 + δ / 4<VAR>hδ2 : δ ≤ 1<VAR>i j : Fin N.succ<VAR>inej : i ≠ j<VAR>hi : ‖a.c i‖ ≤ 2<VAR>hj : 2 < ‖a.c j‖<GOAL>1 - δ ≤ ‖a.c i - (2 / ‖a.c j‖) • a.c j‖
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>N : ℕ<VAR>τ : ℝ<VAR>a : Besicovitch.SatelliteConfig E N τ<VAR>lastc : a.c (Fin.last N) = 0<VAR>lastr : a.r (Fin.last N) = 1<VAR>hτ : 1 ≤ τ<VAR>δ : ℝ<VAR>hδ1 : τ ≤ 1 + δ / 4<VAR>i j : Fin N.succ<VAR>inej : i ≠ j<VAR>hi : 2 < ‖a.c i‖<VAR>hij : ‖a.c i‖ ≤ ‖a.c j‖<GOAL>1 - δ ≤ ‖(2 / ‖a.c i‖) • a.c i - (2 / ‖a.c j‖) • a.c j‖
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>N : ℕ<VAR>τ : ℝ<VAR>a : Besicovitch.SatelliteConfig E N τ<VAR>lastc : a.c (Fin.last N) = 0<VAR>lastr : a.r (Fin.last N) = 1<VAR>hτ : 1 ≤ τ<VAR>δ : ℝ<VAR>hδ1 : τ ≤ 1 + δ / 4<VAR>hδ2 : δ ≤ 1<GOAL>∃ c', (∀ (n : Fin N.succ), ‖c' n‖ ≤ 2) ∧ Pairwise fun i j => 1 - δ ≤ ‖c' i - c' j‖
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<GOAL>IsEmpty (Besicovitch.SatelliteConfig E (Besicovitch.multiplicity E) (Besicovitch.goodτ E))
<VAR>α : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>MeasurableSpace X<VAR>BorelSpace X<VAR>R1Space X<VAR>TopologicalSpace Y<VAR>MeasurableSpace Y<VAR>BorelSpace Y<VAR>R1Space Y<VAR>μ : MeasureTheory.Measure X<VAR>ν : MeasureTheory.Measure Y<VAR>μ.InnerRegularCompactLTTop<VAR>MeasureTheory.IsLocallyFiniteMeasure ν<VAR>l : Filter α<VAR>f : α → C(X, Y)<VAR>g : C(X, Y)<VAR>s : Set Y<VAR>hfg : Filter.Tendsto f l (𝓝 g)<VAR>hf : ∀ᶠ (a : α) in l, MeasureTheory.MeasurePreserving (⇑(f a)) μ ν<VAR>hg : MeasureTheory.MeasurePreserving (⇑g) μ ν<VAR>hs : MeasurableSet s<VAR>hνs : ν s ≠ ⊤<GOAL>Filter.Tendsto (fun a => μ ((⇑(f a) ⁻¹' s) ∆ (⇑g ⁻¹' s))) l (𝓝 0)
<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>MeasurableSpace X<VAR>BorelSpace X<VAR>R1Space X<VAR>TopologicalSpace Y<VAR>MeasurableSpace Y<VAR>BorelSpace Y<VAR>R1Space Y<VAR>μ : MeasureTheory.Measure X<VAR>ν : MeasureTheory.Measure Y<VAR>μ.InnerRegularCompactLTTop<VAR>MeasureTheory.IsLocallyFiniteMeasure ν<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>Fact (1 ≤ p)<VAR>hp : p ≠ ⊤<GOAL>Continuous fun gf => (MeasureTheory.Lp.compMeasurePreserving ⇑↑gf.2 ⋯) gf.1
<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>MeasurableSpace X<VAR>BorelSpace X<VAR>R1Space X<VAR>TopologicalSpace Y<VAR>MeasurableSpace Y<VAR>BorelSpace Y<VAR>R1Space Y<VAR>μ : MeasureTheory.Measure X<VAR>ν : MeasureTheory.Measure Y<VAR>μ.InnerRegularCompactLTTop<VAR>MeasureTheory.IsLocallyFiniteMeasure ν<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>Fact (1 ≤ p)<VAR>α : Type u_5<VAR>l : Filter α<VAR>f : α → ↥(MeasureTheory.Lp E p ν)<VAR>f₀ : ↥(MeasureTheory.Lp E p ν)<VAR>g : α → C(X, Y)<VAR>g₀ : C(X, Y)<VAR>hf : Filter.Tendsto f l (𝓝 f₀)<VAR>hg : Filter.Tendsto g l (𝓝 g₀)<VAR>hgm : ∀ (a : α), MeasureTheory.MeasurePreserving (⇑(g a)) μ ν<VAR>hgm₀ : MeasureTheory.MeasurePreserving (⇑g₀) μ ν<VAR>hp : p ≠ ⊤<GOAL>Filter.Tendsto (fun a => (MeasureTheory.Lp.compMeasurePreserving ⇑(g a) ⋯) (f a)) l (𝓝 ((MeasureTheory.Lp.compMeasurePreserving (⇑g₀) hgm₀) f₀))
<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>MeasurableSpace X<VAR>BorelSpace X<VAR>R1Space X<VAR>TopologicalSpace Y<VAR>MeasurableSpace Y<VAR>BorelSpace Y<VAR>R1Space Y<VAR>μ : MeasureTheory.Measure X<VAR>ν : MeasureTheory.Measure Y<VAR>μ.InnerRegularCompactLTTop<VAR>MeasureTheory.IsLocallyFiniteMeasure ν<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>Fact (1 ≤ p)<VAR>Z : Type u_5<VAR>TopologicalSpace Z<VAR>f : Z → ↥(MeasureTheory.Lp E p ν)<VAR>g : Z → C(X, Y)<VAR>s : Set Z<VAR>z : Z<VAR>hf : ContinuousWithinAt f s z<VAR>hg : ContinuousWithinAt g s z<VAR>hgm : ∀ (z : Z), MeasureTheory.MeasurePreserving (⇑(g z)) μ ν<VAR>hp : p ≠ ⊤<GOAL>ContinuousWithinAt (fun z => (MeasureTheory.Lp.compMeasurePreserving ⇑(g z) ⋯) (f z)) s z
<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>MeasurableSpace X<VAR>BorelSpace X<VAR>R1Space X<VAR>TopologicalSpace Y<VAR>MeasurableSpace Y<VAR>BorelSpace Y<VAR>R1Space Y<VAR>μ : MeasureTheory.Measure X<VAR>ν : MeasureTheory.Measure Y<VAR>μ.InnerRegularCompactLTTop<VAR>MeasureTheory.IsLocallyFiniteMeasure ν<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>Fact (1 ≤ p)<VAR>Z : Type u_5<VAR>TopologicalSpace Z<VAR>f : Z → ↥(MeasureTheory.Lp E p ν)<VAR>g : Z → C(X, Y)<VAR>z : Z<VAR>hf : ContinuousAt f z<VAR>hg : ContinuousAt g z<VAR>hgm : ∀ (z : Z), MeasureTheory.MeasurePreserving (⇑(g z)) μ ν<VAR>hp : p ≠ ⊤<GOAL>ContinuousAt (fun z => (MeasureTheory.Lp.compMeasurePreserving ⇑(g z) ⋯) (f z)) z
<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>MeasurableSpace X<VAR>BorelSpace X<VAR>R1Space X<VAR>TopologicalSpace Y<VAR>MeasurableSpace Y<VAR>BorelSpace Y<VAR>R1Space Y<VAR>μ : MeasureTheory.Measure X<VAR>ν : MeasureTheory.Measure Y<VAR>μ.InnerRegularCompactLTTop<VAR>MeasureTheory.IsLocallyFiniteMeasure ν<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>Fact (1 ≤ p)<VAR>Z : Type u_5<VAR>TopologicalSpace Z<VAR>f : Z → ↥(MeasureTheory.Lp E p ν)<VAR>g : Z → C(X, Y)<VAR>s : Set Z<VAR>hf : ContinuousOn f s<VAR>hg : ContinuousOn g s<VAR>hgm : ∀ (z : Z), MeasureTheory.MeasurePreserving (⇑(g z)) μ ν<VAR>hp : p ≠ ⊤<GOAL>ContinuousOn (fun z => (MeasureTheory.Lp.compMeasurePreserving ⇑(g z) ⋯) (f z)) s
<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>MeasurableSpace X<VAR>BorelSpace X<VAR>R1Space X<VAR>TopologicalSpace Y<VAR>MeasurableSpace Y<VAR>BorelSpace Y<VAR>R1Space Y<VAR>μ : MeasureTheory.Measure X<VAR>ν : MeasureTheory.Measure Y<VAR>μ.InnerRegularCompactLTTop<VAR>MeasureTheory.IsLocallyFiniteMeasure ν<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>Fact (1 ≤ p)<VAR>Z : Type u_5<VAR>TopologicalSpace Z<VAR>f : Z → ↥(MeasureTheory.Lp E p ν)<VAR>g : Z → C(X, Y)<VAR>hf : Continuous f<VAR>hg : Continuous g<VAR>hgm : ∀ (z : Z), MeasureTheory.MeasurePreserving (⇑(g z)) μ ν<VAR>hp : p ≠ ⊤<GOAL>Continuous fun z => (MeasureTheory.Lp.compMeasurePreserving ⇑(g z) ⋯) (f z)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ<VAR>h : MeasureTheory.Memℒp f 2 μ<GOAL>MeasureTheory.Integrable (fun x => f x ^ 2) μ
<VAR>α : Type u_1<VAR>F : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup F<VAR>f : α → F<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<GOAL>MeasureTheory.Memℒp f 2 μ ↔ MeasureTheory.Integrable (fun x => ‖f x‖ ^ 2) μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<GOAL>MeasureTheory.Memℒp f 2 μ ↔ MeasureTheory.Integrable (fun x => f x ^ 2) μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>E : Type u_2<VAR>𝕜 : Type u_3<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>c : E<VAR>f : α → E<VAR>hf : MeasureTheory.Memℒp f p μ<GOAL>MeasureTheory.Memℒp (fun a => ⟪c, f a⟫_𝕜) p μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>E : Type u_2<VAR>𝕜 : Type u_3<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>f : α → E<VAR>hf : MeasureTheory.Memℒp f p μ<VAR>c : E<GOAL>MeasureTheory.Memℒp (fun a => ⟪f a, c⟫_𝕜) p μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>E : Type u_2<VAR>𝕜 : Type u_3<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>f : α → E<VAR>c : E<VAR>hf : MeasureTheory.Integrable f μ<GOAL>MeasureTheory.Integrable (fun x => ⟪c, f x⟫_𝕜) μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>E : Type u_2<VAR>𝕜 : Type u_3<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>f : α → E<VAR>hf : MeasureTheory.Integrable f μ<VAR>c : E<GOAL>MeasureTheory.Integrable (fun x => ⟪f x, c⟫_𝕜) μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>E : Type u_2<VAR>𝕜 : Type u_3<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>CompleteSpace E<VAR>NormedSpace ℝ E<VAR>f : α → E<VAR>hf : MeasureTheory.Integrable f μ<VAR>c : E<GOAL>∫ (x : α), ⟪c, f x⟫_𝕜 ∂μ = ⟪c, ∫ (x : α), f x ∂μ⟫_𝕜
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>E : Type u_2<VAR>𝕜 : Type u_3<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>CompleteSpace E<VAR>NormedSpace ℝ E<VAR>f : α → E<VAR>hf : MeasureTheory.Integrable f μ<VAR>hf_int : ∀ (c : E), ∫ (x : α), ⟪c, f x⟫_𝕜 ∂μ = 0<GOAL>∫ (x : α), f x ∂μ = 0
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup F<VAR>f : ↥(MeasureTheory.Lp F 2 μ)<GOAL>MeasureTheory.eLpNorm (fun x => ‖↑↑f x‖ ^ 2) 1 μ < ⊤
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>𝕜 : Type u_4<VAR>RCLike 𝕜<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>f g : ↥(MeasureTheory.Lp E 2 μ)<GOAL>MeasureTheory.eLpNorm (fun x => ⟪↑↑f x, ↑↑g x⟫_𝕜) 1 μ < ⊤
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>𝕜 : Type u_4<VAR>RCLike 𝕜<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>f g : ↥(MeasureTheory.Lp E 2 μ)<GOAL>⟪f, g⟫_𝕜 = ∫ (a : α), ⟪↑↑f a, ↑↑g a⟫_𝕜 ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>𝕜 : Type u_4<VAR>RCLike 𝕜<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>f : ↥(MeasureTheory.Lp E 2 μ)<GOAL>∫ (a : α), ⟪↑↑f a, ↑↑f a⟫_𝕜 ∂μ = ↑(∫⁻ (a : α), ↑‖↑↑f a‖₊ ^ 2 ∂μ).toReal
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>𝕜 : Type u_4<VAR>RCLike 𝕜<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>f : ↥(MeasureTheory.Lp E 2 μ)<GOAL>‖f‖ ^ 2 = RCLike.re ⟪f, f⟫_𝕜
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>𝕜 : Type u_4<VAR>RCLike 𝕜<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>f g : ↥(MeasureTheory.Lp E 2 μ)<GOAL>MeasureTheory.AEEqFun.mk (fun x => ⟪↑↑f x, ↑↑g x⟫_𝕜) ⋯ ∈ MeasureTheory.Lp 𝕜 1 μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>𝕜 : Type u_4<VAR>RCLike 𝕜<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>f g : ↥(MeasureTheory.Lp E 2 μ)<GOAL>MeasureTheory.Integrable (fun x => ⟪↑↑f x, ↑↑g x⟫_𝕜) μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>𝕜 : Type u_4<VAR>RCLike 𝕜<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>f f' g : ↥(MeasureTheory.Lp E 2 μ)<GOAL>⟪f + f', g⟫_𝕜 = ⟪f, g⟫_𝕜 + ⟪f', g⟫_𝕜
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>𝕜 : Type u_4<VAR>RCLike 𝕜<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>f g : ↥(MeasureTheory.Lp E 2 μ)<VAR>r : 𝕜<GOAL>⟪r • f, g⟫_𝕜 = (starRingEnd 𝕜) r * ⟪f, g⟫_𝕜
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>𝕜 : Type u_4<VAR>RCLike 𝕜<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>s : Set α<VAR>f : ↥(MeasureTheory.Lp E 2 μ)<VAR>hs : MeasurableSet s<VAR>c : E<VAR>hμs : μ s ≠ ⊤<GOAL>⟪MeasureTheory.indicatorConstLp 2 hs hμs c, f⟫_𝕜 = ∫ (x : α) in s, ⟪c, ↑↑f x⟫_𝕜 ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>𝕜 : Type u_4<VAR>RCLike 𝕜<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>s : Set α<VAR>CompleteSpace E<VAR>NormedSpace ℝ E<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>c : E<VAR>f : ↥(MeasureTheory.Lp E 2 μ)<GOAL>⟪MeasureTheory.indicatorConstLp 2 hs hμs c, f⟫_𝕜 = ⟪c, ∫ (x : α) in s, ↑↑f x ∂μ⟫_𝕜
<VAR>α : Type u_1<VAR>𝕜 : Type u_4<VAR>RCLike 𝕜<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>f : ↥(MeasureTheory.Lp 𝕜 2 μ)<GOAL>⟪MeasureTheory.indicatorConstLp 2 hs hμs 1, f⟫_𝕜 = ∫ (x : α) in s, ↑↑f x ∂μ
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>BorelSpace α<VAR>RCLike 𝕜<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>f g : BoundedContinuousFunction α 𝕜<GOAL>⟪(BoundedContinuousFunction.toLp 2 μ 𝕜) f, (BoundedContinuousFunction.toLp 2 μ 𝕜) g⟫_𝕜 = ∫ (x : α), (starRingEnd 𝕜) (f x) * g x ∂μ
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>BorelSpace α<VAR>RCLike 𝕜<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>CompactSpace α<VAR>f g : C(α, 𝕜)<GOAL>⟪(ContinuousMap.toLp 2 μ 𝕜) f, (ContinuousMap.toLp 2 μ 𝕜) g⟫_𝕜 = ∫ (x : α), (starRingEnd 𝕜) (f x) * g x ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>q : ℝ<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>hm : m ≤ m0<VAR>f : α → E<VAR>hf : MeasureTheory.StronglyMeasurable f<GOAL>MeasureTheory.eLpNorm' f q (μ.trim hm) = MeasureTheory.eLpNorm' f q μ
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>hm : m ≤ m0<VAR>f : α → ENNReal<VAR>hf : Measurable f<GOAL>Filter.limsup f (MeasureTheory.ae (μ.trim hm)) = Filter.limsup f (MeasureTheory.ae μ)
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>hm : m ≤ m0<VAR>f : α → ENNReal<VAR>hf : Measurable f<GOAL>essSup f (μ.trim hm) = essSup f μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>hm : m ≤ m0<VAR>f : α → E<VAR>hf : MeasureTheory.StronglyMeasurable f<GOAL>MeasureTheory.eLpNormEssSup f (μ.trim hm) = MeasureTheory.eLpNormEssSup f μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>p : ENNReal<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>hm : m ≤ m0<VAR>f : α → E<VAR>hf : MeasureTheory.StronglyMeasurable f<GOAL>MeasureTheory.eLpNorm f p (μ.trim hm) = MeasureTheory.eLpNorm f p μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>p : ENNReal<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>hm : m ≤ m0<VAR>f : α → E<VAR>hf : MeasureTheory.AEStronglyMeasurable f (μ.trim hm)<GOAL>MeasureTheory.eLpNorm f p (μ.trim hm) = MeasureTheory.eLpNorm f p μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>p : ENNReal<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>hm : m ≤ m0<VAR>f : α → E<VAR>hf : MeasureTheory.Memℒp f p (μ.trim hm)<GOAL>MeasureTheory.Memℒp f p μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace β<VAR>g : α → β<VAR>γ : Type u_4<GOAL>∀ {x : MeasurableSpace γ} {x_1 : MeasurableSpace α} {f : γ → α} {μ : MeasureTheory.Measure γ} {ν : MeasureTheory.Measure α}, MeasureTheory.AEStronglyMeasurable g ν → MeasureTheory.MeasurePreserving f μ ν → MeasureTheory.AEStronglyMeasurable (g ∘ f) μ
<VAR>α : Type u_1<VAR>γ : Type u_3<VAR>TopologicalSpace γ<VAR>β : Type u_4<VAR>f : α → β<VAR>mα : MeasurableSpace α<VAR>μa : MeasureTheory.Measure α<VAR>mβ : MeasurableSpace β<VAR>μb : MeasureTheory.Measure β<VAR>hf : MeasureTheory.MeasurePreserving f μa μb<VAR>h₂ : MeasurableEmbedding f<VAR>g : β → γ<GOAL>MeasureTheory.AEStronglyMeasurable (g ∘ f) μa ↔ MeasureTheory.AEStronglyMeasurable g μb
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>𝕜 : Type u_4<VAR>NontriviallyNormedField 𝕜<VAR>CompleteSpace 𝕜<VAR>E : Type u_5<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f : α → 𝕜<VAR>c : E<VAR>hc : c ≠ 0<GOAL>MeasureTheory.AEStronglyMeasurable (fun x => f x • c) μ ↔ MeasureTheory.AEStronglyMeasurable f μ
<VAR>α : Type u_1<VAR>𝕜 : Type u_4<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_5<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_6<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>_m : MeasurableSpace α<VAR>φ : α → F →L[𝕜] E<VAR>hφ : MeasureTheory.StronglyMeasurable φ<VAR>v : F<GOAL>MeasureTheory.StronglyMeasurable fun a => (φ a) v
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>𝕜 : Type u_4<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_5<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_6<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>φ : α → F →L[𝕜] E<VAR>hφ : MeasureTheory.AEStronglyMeasurable φ μ<VAR>v : F<GOAL>MeasureTheory.AEStronglyMeasurable (fun a => (φ a) v) μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>𝕜 : Type u_4<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_5<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_6<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_7<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>L : E →L[𝕜] F →L[𝕜] G<VAR>f : α → E<VAR>g : α → F<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<VAR>hg : MeasureTheory.AEStronglyMeasurable g μ<GOAL>MeasureTheory.AEStronglyMeasurable (fun x => (L (f x)) (g x)) μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : α → ℝ≥0<VAR>hf : Measurable f<VAR>g : α → E<GOAL>MeasureTheory.AEStronglyMeasurable g (μ.withDensity fun x => ↑(f x)) ↔ MeasureTheory.AEStronglyMeasurable (fun x => ↑(f x) • g x) μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>NormedAddCommGroup E<VAR>f : X → E<VAR>μ : MeasureTheory.Measure X<VAR>s : Set X<VAR>hf : MeasureTheory.LocallyIntegrableOn f s μ<VAR>t : Set X<VAR>hst : t ⊆ s<GOAL>MeasureTheory.LocallyIntegrableOn f t μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>NormedAddCommGroup E<VAR>f : X → E<VAR>μ : MeasureTheory.Measure X<VAR>s : Set X<VAR>hf : MeasureTheory.LocallyIntegrableOn f s μ<GOAL>MeasureTheory.LocallyIntegrableOn (fun x => ‖f x‖) s μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>F : Type u_4<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>f : X → E<VAR>μ : MeasureTheory.Measure X<VAR>s : Set X<VAR>hf : MeasureTheory.LocallyIntegrableOn f s μ<VAR>g : X → F<VAR>hg : MeasureTheory.AEStronglyMeasurable g μ<VAR>h : ∀ᵐ (x : X) ∂μ, ‖g x‖ ≤ ‖f x‖<GOAL>MeasureTheory.LocallyIntegrableOn g s μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>NormedAddCommGroup E<VAR>f : X → E<VAR>μ : MeasureTheory.Measure X<VAR>s : Set X<VAR>hf : MeasureTheory.IntegrableOn f s μ<GOAL>MeasureTheory.LocallyIntegrableOn f s μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>NormedAddCommGroup E<VAR>f : X → E<VAR>μ : MeasureTheory.Measure X<VAR>s : Set X<VAR>hf : MeasureTheory.LocallyIntegrableOn f s μ<VAR>hs : IsCompact s<GOAL>MeasureTheory.IntegrableOn f s μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>NormedAddCommGroup E<VAR>f : X → E<VAR>μ : MeasureTheory.Measure X<VAR>s : Set X<VAR>hf : MeasureTheory.LocallyIntegrableOn f s μ<VAR>t : Set X<VAR>hst : t ⊆ s<VAR>ht : IsCompact t<GOAL>MeasureTheory.IntegrableOn f t μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>NormedAddCommGroup E<VAR>f : X → E<VAR>μ : MeasureTheory.Measure X<VAR>s : Set X<VAR>SecondCountableTopology X<VAR>hf : MeasureTheory.LocallyIntegrableOn f s μ<GOAL>∃ T, T.Countable ∧ (∀ u ∈ T, IsOpen u) ∧ s ⊆ ⋃ u ∈ T, u ∧ ∀ u ∈ T, MeasureTheory.IntegrableOn f (u ∩ s) μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>NormedAddCommGroup E<VAR>f : X → E<VAR>μ : MeasureTheory.Measure X<VAR>s : Set X<VAR>SecondCountableTopology X<VAR>hf : MeasureTheory.LocallyIntegrableOn f s μ<GOAL>∃ u, (∀ (n : ℕ), IsOpen (u n)) ∧ s ⊆ ⋃ n, u n ∧ ∀ (n : ℕ), MeasureTheory.IntegrableOn f (u n ∩ s) μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>NormedAddCommGroup E<VAR>f : X → E<VAR>μ : MeasureTheory.Measure X<VAR>s : Set X<VAR>SecondCountableTopology X<VAR>hf : MeasureTheory.LocallyIntegrableOn f s μ<GOAL>MeasureTheory.AEStronglyMeasurable f (μ.restrict s)
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>NormedAddCommGroup E<VAR>f : X → E<VAR>μ : MeasureTheory.Measure X<VAR>s : Set X<VAR>LocallyCompactSpace X<VAR>T2Space X<VAR>hs : IsClosed s ∨ IsOpen s<GOAL>MeasureTheory.LocallyIntegrableOn f s μ ↔ ∀ k ⊆ s, IsCompact k → MeasureTheory.IntegrableOn f k μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>NormedAddCommGroup E<VAR>f g : X → E<VAR>μ : MeasureTheory.Measure X<VAR>s : Set X<VAR>hf : MeasureTheory.LocallyIntegrableOn f s μ<VAR>hg : MeasureTheory.LocallyIntegrableOn g s μ<GOAL>MeasureTheory.LocallyIntegrableOn (f + g) s μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>NormedAddCommGroup E<VAR>f g : X → E<VAR>μ : MeasureTheory.Measure X<VAR>s : Set X<VAR>hf : MeasureTheory.LocallyIntegrableOn f s μ<VAR>hg : MeasureTheory.LocallyIntegrableOn g s μ<GOAL>MeasureTheory.LocallyIntegrableOn (f - g) s μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>NormedAddCommGroup E<VAR>f : X → E<VAR>μ : MeasureTheory.Measure X<VAR>s : Set X<VAR>hf : MeasureTheory.LocallyIntegrableOn f s μ<GOAL>MeasureTheory.LocallyIntegrableOn (-f) s μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>NormedAddCommGroup E<VAR>f : X → E<VAR>μ : MeasureTheory.Measure X<VAR>s : Set X<VAR>hs : MeasurableSet s<GOAL>MeasureTheory.LocallyIntegrable (fun x => f ↑x) (MeasureTheory.Measure.comap Subtype.val μ) ↔ MeasureTheory.LocallyIntegrableOn f s μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>NormedAddCommGroup E<VAR>f : X → E<VAR>μ : MeasureTheory.Measure X<GOAL>MeasureTheory.LocallyIntegrableOn f Set.univ μ ↔ MeasureTheory.LocallyIntegrable f μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>NormedAddCommGroup E<VAR>f : X → E<VAR>μ : MeasureTheory.Measure X<VAR>hf : MeasureTheory.LocallyIntegrable f μ<VAR>s : Set X<GOAL>MeasureTheory.LocallyIntegrableOn f s μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>NormedAddCommGroup E<VAR>f : X → E<VAR>μ : MeasureTheory.Measure X<VAR>hf : MeasureTheory.Integrable f μ<GOAL>MeasureTheory.LocallyIntegrable f μ