ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>G : Type u_3<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>ι : Type u_4<VAR>Countable ι<VAR>F : ι → α → G<VAR>f : α → G<VAR>bound : ι → α → ℝ<VAR>hF_meas : ∀ (n : ι), MeasureTheory.AEStronglyMeasurable (F n) μ<VAR>h_bound : ∀ (n : ι), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound n a<VAR>bound_summable : ∀ᵐ (a : α) ∂μ, Summable fun n => bound n a<VAR>bound_integrable : MeasureTheory.Integrable (fun a => ∑' (n : ι), bound n a) μ<VAR>h_lim : ∀ᵐ (a : α) ∂μ, HasSum (fun n => F n a) (f a)<GOAL>HasSum (fun n => ∫ (a : α), F n a ∂μ) (∫ (a : α), f a ∂μ)
<VAR>α : Type u_1<VAR>G : Type u_3<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>ι : Type u_4<VAR>Countable ι<VAR>f : ι → α → G<VAR>hf : ∀ (i : ι), MeasureTheory.AEStronglyMeasurable (f i) μ<VAR>hf' : ∑' (i : ι), ∫⁻ (a : α), ↑‖f i a‖₊ ∂μ ≠ ⊤<GOAL>∫ (a : α), ∑' (i : ι), f i a ∂μ = ∑' (i : ι), ∫ (a : α), f i a ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>ι : Type u_4<VAR>Countable ι<VAR>F : ι → α → E<VAR>hF_int : ∀ (i : ι), MeasureTheory.Integrable (F i) μ<VAR>hF_sum : Summable fun i => ∫ (a : α), ‖F i a‖ ∂μ<GOAL>HasSum (fun x => ∫ (a : α), F x a ∂μ) (∫ (a : α), ∑' (i : ι), F i a ∂μ)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>ι : Type u_4<VAR>Countable ι<VAR>F : ι → α → E<VAR>hF_int : ∀ (i : ι), MeasureTheory.Integrable (F i) μ<VAR>hF_sum : Summable fun i => ∫ (a : α), ‖F i a‖ ∂μ<GOAL>∑' (i : ι), ∫ (a : α), F i a ∂μ = ∫ (a : α), ∑' (i : ι), F i a ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>s : ℕ → Set α<VAR>f : α → E<VAR>hsm : ∀ (i : ℕ), MeasurableSet (s i)<VAR>h_anti : Antitone s<VAR>hfi : MeasureTheory.IntegrableOn f (s 0) μ<GOAL>Filter.Tendsto (fun i => ∫ (a : α) in s i, f a ∂μ) Filter.atTop (nhds (∫ (a : α) in ⋂ n, s n, f a ∂μ))
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>a b : ℝ<VAR>f : ℝ → E<VAR>μ : MeasureTheory.Measure ℝ<VAR>ι : Type u_5<VAR>l : Filter ι<VAR>l.IsCountablyGenerated<VAR>F : ι → ℝ → E<VAR>bound : ℝ → ℝ<VAR>hF_meas : ∀ᶠ (n : ι) in l, MeasureTheory.AEStronglyMeasurable (F n) (μ.restrict (Ι a b))<VAR>h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (x : ℝ) ∂μ, x ∈ Ι a b → ‖F n x‖ ≤ bound x<VAR>bound_integrable : IntervalIntegrable bound μ a b<VAR>h_lim : ∀ᵐ (x : ℝ) ∂μ, x ∈ Ι a b → Filter.Tendsto (fun n => F n x) l (nhds (f x))<GOAL>Filter.Tendsto (fun n => ∫ (x : ℝ) in a..b, F n x ∂μ) l (nhds (∫ (x : ℝ) in a..b, f x ∂μ))
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>a b : ℝ<VAR>f : ℝ → E<VAR>μ : MeasureTheory.Measure ℝ<VAR>ι : Type u_5<VAR>Countable ι<VAR>F : ι → ℝ → E<VAR>bound : ι → ℝ → ℝ<VAR>hF_meas : ∀ (n : ι), MeasureTheory.AEStronglyMeasurable (F n) (μ.restrict (Ι a b))<VAR>h_bound : ∀ (n : ι), ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → ‖F n t‖ ≤ bound n t<VAR>bound_summable : ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → Summable fun n => bound n t<VAR>bound_integrable : IntervalIntegrable (fun t => ∑' (n : ι), bound n t) μ a b<VAR>h_lim : ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → HasSum (fun n => F n t) (f t)<GOAL>HasSum (fun n => ∫ (t : ℝ) in a..b, F n t ∂μ) (∫ (t : ℝ) in a..b, f t ∂μ)
<VAR>ι : Type u_1<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>a b : ℝ<VAR>Countable ι<VAR>f : ι → C(ℝ, E)<VAR>hf_sum : Summable fun i => ‖ContinuousMap.restrict (↑{ carrier := Set.uIcc a b, isCompact' := ⋯ }) (f i)‖<GOAL>HasSum (fun i => ∫ (x : ℝ) in a..b, (f i) x) (∫ (x : ℝ) in a..b, ∑' (i : ι), (f i) x)
<VAR>ι : Type u_1<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>a b : ℝ<VAR>Countable ι<VAR>f : ι → C(ℝ, E)<VAR>hf_sum : Summable fun i => ‖ContinuousMap.restrict (↑{ carrier := Set.uIcc a b, isCompact' := ⋯ }) (f i)‖<GOAL>∑' (i : ι), ∫ (x : ℝ) in a..b, (f i) x = ∫ (x : ℝ) in a..b, ∑' (i : ι), (f i) x
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>μ : MeasureTheory.Measure ℝ<VAR>X : Type u_5<VAR>TopologicalSpace X<VAR>FirstCountableTopology X<VAR>F : X → ℝ → E<VAR>x₀ : X<VAR>bound : ℝ → ℝ<VAR>a b : ℝ<VAR>s : Set X<VAR>hF_meas : ∀ᶠ (x : X) in nhdsWithin x₀ s, MeasureTheory.AEStronglyMeasurable (F x) (μ.restrict (Ι a b))<VAR>h_bound : ∀ᶠ (x : X) in nhdsWithin x₀ s, ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → ‖F x t‖ ≤ bound t<VAR>bound_integrable : IntervalIntegrable bound μ a b<VAR>h_cont : ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → ContinuousWithinAt (fun x => F x t) s x₀<GOAL>ContinuousWithinAt (fun x => ∫ (t : ℝ) in a..b, F x t ∂μ) s x₀
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>μ : MeasureTheory.Measure ℝ<VAR>X : Type u_5<VAR>TopologicalSpace X<VAR>FirstCountableTopology X<VAR>F : X → ℝ → E<VAR>x₀ : X<VAR>bound : ℝ → ℝ<VAR>a b : ℝ<VAR>hF_meas : ∀ᶠ (x : X) in nhds x₀, MeasureTheory.AEStronglyMeasurable (F x) (μ.restrict (Ι a b))<VAR>h_bound : ∀ᶠ (x : X) in nhds x₀, ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → ‖F x t‖ ≤ bound t<VAR>bound_integrable : IntervalIntegrable bound μ a b<VAR>h_cont : ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → ContinuousAt (fun x => F x t) x₀<GOAL>ContinuousAt (fun x => ∫ (t : ℝ) in a..b, F x t ∂μ) x₀
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>μ : MeasureTheory.Measure ℝ<VAR>X : Type u_5<VAR>TopologicalSpace X<VAR>FirstCountableTopology X<VAR>F : X → ℝ → E<VAR>bound : ℝ → ℝ<VAR>a b : ℝ<VAR>hF_meas : ∀ (x : X), MeasureTheory.AEStronglyMeasurable (F x) (μ.restrict (Ι a b))<VAR>h_bound : ∀ (x : X), ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → ‖F x t‖ ≤ bound t<VAR>bound_integrable : IntervalIntegrable bound μ a b<VAR>h_cont : ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → Continuous fun x => F x t<GOAL>Continuous fun x => ∫ (t : ℝ) in a..b, F x t ∂μ
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>a b₀ b₁ b₂ : ℝ<VAR>μ : MeasureTheory.Measure ℝ<VAR>f : ℝ → E<VAR>hb₀ : μ {b₀} = 0<VAR>h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)<GOAL>ContinuousWithinAt (fun b => ∫ (x : ℝ) in a..b, f x ∂μ) (Set.Icc b₁ b₂) b₀
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>TopologicalSpace X<VAR>μ : MeasureTheory.Measure ℝ<VAR>FirstCountableTopology X<VAR>F : X → ℝ → E<VAR>bound : ℝ → ℝ<VAR>a b : ℝ<VAR>a₀ b₀ : ℝ<VAR>x₀ : X<VAR>hF_meas : ∀ (x : X), MeasureTheory.AEStronglyMeasurable (F x) (μ.restrict (Ι a b))<VAR>h_bound : ∀ᶠ (x : X) in nhds x₀, ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖F x t‖ ≤ bound t<VAR>bound_integrable : IntervalIntegrable bound μ a b<VAR>h_cont : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ContinuousAt (fun x => F x t) x₀<VAR>ha₀ : a₀ ∈ Set.Ioo a b<VAR>hb₀ : b₀ ∈ Set.Ioo a b<VAR>hμb₀ : μ {b₀} = 0<GOAL>ContinuousAt (fun p => ∫ (t : ℝ) in a₀..p.2, F p.1 t ∂μ) (x₀, b₀)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>a b : ℝ<VAR>μ : MeasureTheory.Measure ℝ<VAR>f : ℝ → E<VAR>MeasureTheory.NoAtoms μ<VAR>h_int : MeasureTheory.IntegrableOn f (Set.Icc a b) μ<GOAL>ContinuousOn (fun x => ∫ (t : ℝ) in Set.Ioc a x, f t ∂μ) (Set.Icc a b)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>a b : ℝ<VAR>μ : MeasureTheory.Measure ℝ<VAR>f : ℝ → E<VAR>MeasureTheory.NoAtoms μ<VAR>h_int : MeasureTheory.IntegrableOn f (Set.Icc a b) μ<GOAL>ContinuousOn (fun x => ∫ (t : ℝ) in Set.Icc a x, f t ∂μ) (Set.Icc a b)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>a b₁ b₂ : ℝ<VAR>μ : MeasureTheory.Measure ℝ<VAR>f : ℝ → E<VAR>MeasureTheory.NoAtoms μ<VAR>h_int : IntervalIntegrable f μ b₁ b₂<VAR>ha : a ∈ Set.uIcc b₁ b₂<GOAL>ContinuousOn (fun b => ∫ (x : ℝ) in a..b, f x ∂μ) (Set.uIcc b₁ b₂)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>a b : ℝ<VAR>μ : MeasureTheory.Measure ℝ<VAR>f : ℝ → E<VAR>MeasureTheory.NoAtoms μ<VAR>h_int : MeasureTheory.IntegrableOn f (Set.uIcc a b) μ<GOAL>ContinuousOn (fun x => ∫ (t : ℝ) in a..x, f t ∂μ) (Set.uIcc a b)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>a b : ℝ<VAR>μ : MeasureTheory.Measure ℝ<VAR>f : ℝ → E<VAR>MeasureTheory.NoAtoms μ<VAR>h_int : MeasureTheory.IntegrableOn f (Set.uIcc a b) μ<GOAL>ContinuousOn (fun x => ∫ (t : ℝ) in x..b, f t ∂μ) (Set.uIcc a b)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>μ : MeasureTheory.Measure ℝ<VAR>f : ℝ → E<VAR>MeasureTheory.NoAtoms μ<VAR>h_int : ∀ (a b : ℝ), IntervalIntegrable f μ a b<VAR>a : ℝ<GOAL>Continuous fun b => ∫ (x : ℝ) in a..b, f x ∂μ
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>μ : MeasureTheory.Measure ℝ<VAR>f : ℝ → E<VAR>MeasureTheory.NoAtoms μ<VAR>h_int : MeasureTheory.Integrable f μ<VAR>a : ℝ<GOAL>Continuous fun b => ∫ (x : ℝ) in a..b, f x ∂μ
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>TopologicalSpace X<VAR>μ : MeasureTheory.Measure ℝ<VAR>MeasureTheory.NoAtoms μ<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>f : X → ℝ → E<VAR>a₀ : ℝ<VAR>hf : Continuous (Function.uncurry f)<GOAL>Continuous fun p => ∫ (t : ℝ) in a₀..p.2, f p.1 t ∂μ
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>TopologicalSpace X<VAR>μ : MeasureTheory.Measure ℝ<VAR>MeasureTheory.NoAtoms μ<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>f : X → ℝ → E<VAR>a₀ : ℝ<VAR>hf : Continuous (Function.uncurry f)<VAR>s : X → ℝ<VAR>hs : Continuous s<GOAL>Continuous fun x => ∫ (t : ℝ) in a₀..s x, f x t ∂μ
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>TopologicalSpace X<VAR>μ : MeasureTheory.Measure ℝ<VAR>MeasureTheory.NoAtoms μ<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>f : X → ℝ → E<VAR>hf : Continuous (Function.uncurry f)<VAR>a₀ b₀ : ℝ<GOAL>Continuous fun x => ∫ (t : ℝ) in a₀..b₀, f x t ∂μ
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>SecondCountableTopology α<VAR>MeasurableSpace α<VAR>BorelSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>IsUnifLocDoublingMeasure μ<VAR>p : ℕ → Prop<VAR>s : ℕ → Set α<VAR>hs : ∀ (i : ℕ), IsClosed (s i)<VAR>r₁ r₂ : ℕ → ℝ<VAR>hr : Filter.Tendsto r₁ Filter.atTop (𝓝[>] 0)<VAR>hrp : 0 ≤ r₁<VAR>M : ℝ<VAR>hM : 0 < M<VAR>hM' : M < 1<VAR>hMr : ∀ᶠ (i : ℕ) in Filter.atTop, M * r₁ i ≤ r₂ i<GOAL>Filter.blimsup (fun i => Metric.cthickening (r₁ i) (s i)) Filter.atTop p ≤ᵐ[μ] Filter.blimsup (fun i => Metric.cthickening (r₂ i) (s i)) Filter.atTop p
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>SecondCountableTopology α<VAR>MeasurableSpace α<VAR>BorelSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>IsUnifLocDoublingMeasure μ<VAR>p : ℕ → Prop<VAR>s : ℕ → Set α<VAR>M : ℝ<VAR>hM : 0 < M<VAR>r₁ r₂ : ℕ → ℝ<VAR>hr : Filter.Tendsto r₁ Filter.atTop (𝓝[>] 0)<VAR>hMr : ∀ᶠ (i : ℕ) in Filter.atTop, M * r₁ i ≤ r₂ i<GOAL>Filter.blimsup (fun i => Metric.cthickening (r₁ i) (s i)) Filter.atTop p ≤ᵐ[μ] Filter.blimsup (fun i => Metric.cthickening (r₂ i) (s i)) Filter.atTop p
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>SecondCountableTopology α<VAR>MeasurableSpace α<VAR>BorelSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>IsUnifLocDoublingMeasure μ<VAR>p : ℕ → Prop<VAR>s : ℕ → Set α<VAR>M : ℝ<VAR>hM : 0 < M<VAR>r : ℕ → ℝ<VAR>hr : Filter.Tendsto r Filter.atTop (𝓝 0)<GOAL>Filter.blimsup (fun i => Metric.cthickening (M * r i) (s i)) Filter.atTop p =ᵐ[μ] Filter.blimsup (fun i => Metric.cthickening (r i) (s i)) Filter.atTop p
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>SecondCountableTopology α<VAR>MeasurableSpace α<VAR>BorelSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>IsUnifLocDoublingMeasure μ<VAR>p : ℕ → Prop<VAR>s : ℕ → Set α<VAR>r : ℕ → ℝ<VAR>hr : Filter.Tendsto r Filter.atTop (𝓝 0)<VAR>hr' : ∀ᶠ (i : ℕ) in Filter.atTop, p i → 0 < r i<GOAL>Filter.blimsup (fun i => Metric.cthickening (r i) (s i)) Filter.atTop p =ᵐ[μ] Filter.blimsup (fun i => Metric.thickening (r i) (s i)) Filter.atTop p
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>SecondCountableTopology α<VAR>MeasurableSpace α<VAR>BorelSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>IsUnifLocDoublingMeasure μ<VAR>p : ℕ → Prop<VAR>s : ℕ → Set α<VAR>M : ℝ<VAR>hM : 0 < M<VAR>r : ℕ → ℝ<VAR>hr : Filter.Tendsto r Filter.atTop (𝓝 0)<VAR>hr' : ∀ᶠ (i : ℕ) in Filter.atTop, p i → 0 < r i<GOAL>Filter.blimsup (fun i => Metric.thickening (M * r i) (s i)) Filter.atTop p =ᵐ[μ] Filter.blimsup (fun i => Metric.thickening (r i) (s i)) Filter.atTop p
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>SecondCountableTopology α<VAR>MeasurableSpace α<VAR>BorelSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>IsUnifLocDoublingMeasure μ<VAR>p : ℕ → Prop<VAR>s : ℕ → Set α<VAR>M : ℝ<VAR>hM : 0 < M<VAR>r : ℕ → ℝ<VAR>hr : Filter.Tendsto r Filter.atTop (𝓝 0)<GOAL>Filter.blimsup (fun i => Metric.thickening (M * r i) (s i)) Filter.atTop p =ᵐ[μ] Filter.blimsup (fun i => Metric.thickening (r i) (s i)) Filter.atTop p
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>f : α → E<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<VAR>ε : ℝ≥0∞<GOAL>(ε * μ {x | ε ≤ ↑‖f x‖₊ ^ p.toReal}) ^ (1 / p.toReal) ≤ MeasureTheory.eLpNorm f p μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>f : α → E<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<VAR>ε : ℝ≥0∞<GOAL>ε * μ {x | ε ≤ ↑‖f x‖₊ ^ p.toReal} ≤ MeasureTheory.eLpNorm f p μ ^ p.toReal
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>f : α → E<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<VAR>ε : ℝ≥0∞<GOAL>ε ^ p.toReal * μ {x | ε ≤ ↑‖f x‖₊} ≤ MeasureTheory.eLpNorm f p μ ^ p.toReal
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>f : α → E<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<GOAL>μ {x | ε ≤ ↑‖f x‖₊} ≤ ε⁻¹ ^ p.toReal * MeasureTheory.eLpNorm f p μ ^ p.toReal
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>B : ι → Set α<VAR>t : Set ι<VAR>δ : ι → ℝ<VAR>τ : ℝ<VAR>hτ : 1 < τ<VAR>δnonneg : ∀ a ∈ t, 0 ≤ δ a<VAR>R : ℝ<VAR>δle : ∀ a ∈ t, δ a ≤ R<VAR>hne : ∀ a ∈ t, (B a).Nonempty<GOAL>∃ u ⊆ t, u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∃ b ∈ u, (B a ∩ B b).Nonempty ∧ δ a ≤ τ * δ b
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>MetricSpace α<VAR>t : Set ι<VAR>x : ι → α<VAR>r : ι → ℝ<VAR>R : ℝ<VAR>hr : ∀ a ∈ t, r a ≤ R<VAR>τ : ℝ<VAR>hτ : 3 < τ<GOAL>∃ u ⊆ t, (u.PairwiseDisjoint fun a => Metric.closedBall (x a) (r a)) ∧ ∀ a ∈ t, ∃ b ∈ u, Metric.closedBall (x a) (r a) ⊆ Metric.closedBall (x b) (τ * r b)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>MetricSpace α<VAR>MeasurableSpace α<VAR>OpensMeasurableSpace α<VAR>SecondCountableTopology α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>s : Set α<VAR>t : Set ι<VAR>C : ℝ≥0<VAR>r : ι → ℝ<VAR>c : ι → α<VAR>B : ι → Set α<VAR>hB : ∀ a ∈ t, B a ⊆ Metric.closedBall (c a) (r a)<VAR>μB : ∀ a ∈ t, μ (Metric.closedBall (c a) (3 * r a)) ≤ ↑C * μ (B a)<VAR>ht : ∀ a ∈ t, (interior (B a)).Nonempty<VAR>h't : ∀ a ∈ t, IsClosed (B a)<VAR>hf : ∀ x ∈ s, ∀ ε > 0, ∃ a ∈ t, r a ≤ ε ∧ c a = x<GOAL>∃ u ⊆ t, u.Countable ∧ u.PairwiseDisjoint B ∧ μ (s \ ⋃ a ∈ u, B a) = 0
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<GOAL>∀ {x : MeasurableSpace α} {f g : α → E}, MeasureTheory.StronglyMeasurable f → MeasureTheory.StronglyMeasurable g → MeasureTheory.StronglyMeasurable fun t => ⟪f t, g t⟫_𝕜
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>f : α → 𝕜<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<GOAL>MeasureTheory.AEStronglyMeasurable (fun x => RCLike.re (f x)) μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>f : α → 𝕜<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<GOAL>MeasureTheory.AEStronglyMeasurable (fun x => RCLike.im (f x)) μ
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<GOAL>∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → E}, MeasureTheory.AEStronglyMeasurable f μ → MeasureTheory.AEStronglyMeasurable g μ → MeasureTheory.AEStronglyMeasurable (fun x => ⟪f x, g x⟫_𝕜) μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>q : ℝ<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → E<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<VAR>hg : MeasureTheory.AEStronglyMeasurable g μ<VAR>hq1 : 1 ≤ q<GOAL>MeasureTheory.eLpNorm' (f + g) q μ ≤ MeasureTheory.eLpNorm' f q μ + MeasureTheory.eLpNorm' g q μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>q : ℝ<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → E<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<VAR>hq0 : 0 ≤ q<VAR>hq1 : q ≤ 1<GOAL>MeasureTheory.eLpNorm' (f + g) q μ ≤ 2 ^ (1 / q - 1) * (MeasureTheory.eLpNorm' f q μ + MeasureTheory.eLpNorm' g q μ)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → E<GOAL>MeasureTheory.eLpNormEssSup (f + g) μ ≤ MeasureTheory.eLpNormEssSup f μ + MeasureTheory.eLpNormEssSup g μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → E<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<VAR>hg : MeasureTheory.AEStronglyMeasurable g μ<VAR>hp1 : 1 ≤ p<GOAL>MeasureTheory.eLpNorm (f + g) p μ ≤ MeasureTheory.eLpNorm f p μ + MeasureTheory.eLpNorm g p μ
<VAR>p : ℝ≥0∞<VAR>hp : 1 ≤ p<GOAL>MeasureTheory.LpAddConst p = 1
<GOAL>MeasureTheory.LpAddConst 0 = 1
<VAR>p : ℝ≥0∞<GOAL>MeasureTheory.LpAddConst p < ⊤
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → E<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<VAR>hg : MeasureTheory.AEStronglyMeasurable g μ<VAR>p : ℝ≥0∞<GOAL>MeasureTheory.eLpNorm (f + g) p μ ≤ MeasureTheory.LpAddConst p * (MeasureTheory.eLpNorm f p μ + MeasureTheory.eLpNorm g p μ)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure α<VAR>p : ℝ≥0∞<VAR>δ : ℝ≥0∞<VAR>hδ : δ ≠ 0<GOAL>∃ η, 0 < η ∧ ∀ (f g : α → E), MeasureTheory.AEStronglyMeasurable f μ → MeasureTheory.AEStronglyMeasurable g μ → MeasureTheory.eLpNorm f p μ ≤ η → MeasureTheory.eLpNorm g p μ ≤ η → MeasureTheory.eLpNorm (f + g) p μ < δ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → E<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<VAR>hg : MeasureTheory.AEStronglyMeasurable g μ<VAR>p : ℝ≥0∞<GOAL>MeasureTheory.eLpNorm (f - g) p μ ≤ MeasureTheory.LpAddConst p * (MeasureTheory.eLpNorm f p μ + MeasureTheory.eLpNorm g p μ)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → E<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<VAR>hg : MeasureTheory.AEStronglyMeasurable g μ<VAR>hp : 1 ≤ p<GOAL>MeasureTheory.eLpNorm (f - g) p μ ≤ MeasureTheory.eLpNorm f p μ + MeasureTheory.eLpNorm g p μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → E<VAR>hf : MeasureTheory.Memℒp f p μ<VAR>hg : MeasureTheory.Memℒp g p μ<GOAL>MeasureTheory.eLpNorm (f + g) p μ < ⊤
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>q : ℝ<VAR>μ : MeasureTheory.Measure α<VAR>ι : Type u_3<VAR>f : ι → α → E<VAR>s : Finset ι<VAR>hfs : ∀ i ∈ s, MeasureTheory.AEStronglyMeasurable (f i) μ<VAR>hq1 : 1 ≤ q<GOAL>MeasureTheory.eLpNorm' (∑ i ∈ s, f i) q μ ≤ ∑ i ∈ s, MeasureTheory.eLpNorm' (f i) q μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>ι : Type u_3<VAR>f : ι → α → E<VAR>s : Finset ι<VAR>hfs : ∀ i ∈ s, MeasureTheory.AEStronglyMeasurable (f i) μ<VAR>hp1 : 1 ≤ p<GOAL>MeasureTheory.eLpNorm (∑ i ∈ s, f i) p μ ≤ ∑ i ∈ s, MeasureTheory.eLpNorm (f i) p μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → E<VAR>hf : MeasureTheory.Memℒp f p μ<VAR>hg : MeasureTheory.Memℒp g p μ<GOAL>MeasureTheory.Memℒp (f + g) p μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → E<VAR>hf : MeasureTheory.Memℒp f p μ<VAR>hg : MeasureTheory.Memℒp g p μ<GOAL>MeasureTheory.Memℒp (f - g) p μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>ι : Type u_3<VAR>s : Finset ι<VAR>f : ι → α → E<VAR>hf : ∀ i ∈ s, MeasureTheory.Memℒp (f i) p μ<GOAL>MeasureTheory.Memℒp (fun a => ∑ i ∈ s, f i a) p μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>ι : Type u_3<VAR>s : Finset ι<VAR>f : ι → α → E<VAR>hf : ∀ i ∈ s, MeasureTheory.Memℒp (f i) p μ<GOAL>MeasureTheory.Memℒp (∑ i ∈ s, f i) p μ
<VAR>M : Type u_1<VAR>α : Type u_3<VAR>E : Type u_4<VAR>MeasurableSpace M<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure α<VAR>p : ℝ≥0∞<VAR>SMul M α<VAR>MeasureTheory.SMulInvariantMeasure M α μ<VAR>MeasurableSMul M α<VAR>c : Mᵈᵐᵃ<VAR>f : ↥(MeasureTheory.Lp E p μ)<GOAL>↑(c • f) = c • ↑f
<VAR>M : Type u_1<VAR>α : Type u_3<VAR>E : Type u_4<VAR>MeasurableSpace M<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure α<VAR>p : ℝ≥0∞<VAR>VAdd M α<VAR>MeasureTheory.VAddInvariantMeasure M α μ<VAR>MeasurableVAdd M α<VAR>c : Mᵈᵃᵃ<VAR>f : ↥(MeasureTheory.Lp E p μ)<GOAL>↑(c +ᵥ f) = c +ᵥ ↑f
<VAR>M : Type u_1<VAR>α : Type u_3<VAR>E : Type u_4<VAR>MeasurableSpace M<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure α<VAR>p : ℝ≥0∞<VAR>SMul M α<VAR>MeasureTheory.SMulInvariantMeasure M α μ<VAR>MeasurableSMul M α<VAR>c : Mᵈᵐᵃ<VAR>f : ↥(MeasureTheory.Lp E p μ)<GOAL>↑↑(c • f) =ᵐ[μ] fun x => ↑↑f (DomMulAct.mk.symm c • x)
<VAR>M : Type u_1<VAR>α : Type u_3<VAR>E : Type u_4<VAR>MeasurableSpace M<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure α<VAR>p : ℝ≥0∞<VAR>VAdd M α<VAR>MeasureTheory.VAddInvariantMeasure M α μ<VAR>MeasurableVAdd M α<VAR>c : Mᵈᵃᵃ<VAR>f : ↥(MeasureTheory.Lp E p μ)<GOAL>↑↑(c +ᵥ f) =ᵐ[μ] fun x => ↑↑f (DomAddAct.mk.symm c +ᵥ x)
<VAR>M : Type u_1<VAR>α : Type u_3<VAR>E : Type u_4<VAR>MeasurableSpace M<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure α<VAR>p : ℝ≥0∞<VAR>VAdd M α<VAR>MeasureTheory.VAddInvariantMeasure M α μ<VAR>MeasurableVAdd M α<VAR>c : M<VAR>f : α → E<VAR>hf : MeasureTheory.Memℒp f p μ<GOAL>DomAddAct.mk c +ᵥ MeasureTheory.Memℒp.toLp f hf = MeasureTheory.Memℒp.toLp (fun x => f (c +ᵥ x)) ⋯
<VAR>M : Type u_1<VAR>α : Type u_3<VAR>E : Type u_4<VAR>MeasurableSpace M<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure α<VAR>p : ℝ≥0∞<VAR>SMul M α<VAR>MeasureTheory.SMulInvariantMeasure M α μ<VAR>MeasurableSMul M α<VAR>c : M<VAR>f : α → E<VAR>hf : MeasureTheory.Memℒp f p μ<GOAL>DomMulAct.mk c • MeasureTheory.Memℒp.toLp f hf = MeasureTheory.Memℒp.toLp (fun x => f (c • x)) ⋯
<VAR>M : Type u_1<VAR>α : Type u_3<VAR>E : Type u_4<VAR>MeasurableSpace M<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure α<VAR>p : ℝ≥0∞<VAR>SMul M α<VAR>MeasureTheory.SMulInvariantMeasure M α μ<VAR>MeasurableSMul M α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>c : Mᵈᵐᵃ<VAR>a : E<GOAL>c • (MeasureTheory.Lp.const p μ) a = (MeasureTheory.Lp.const p μ) a