ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : MeasureTheory.SimpleFunc α E<VAR>hfi : MeasureTheory.Integrable (↑f) μ<GOAL>∫ (x : α), ↑f x ∂μ = ∑ x ∈ f.range, (μ (↑f ⁻¹' {x})).toReal • x
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>c : E<GOAL>∫ (x : α), c ∂μ = (μ Set.univ).toReal • c
<VAR>α : Type u_1<VAR>G : Type u_5<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>f : α → G<VAR>C : ℝ<VAR>h : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C<GOAL>‖∫ (x : α), f x ∂μ‖ ≤ C * (μ Set.univ).toReal
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>f : α → E<VAR>s : Set E<VAR>TopologicalSpace.SeparableSpace ↑s<VAR>hfi : MeasureTheory.Integrable f μ<VAR>hfm : Measurable f<VAR>hs : ∀ᵐ (x : α) ∂μ, f x ∈ closure s<VAR>y₀ : E<VAR>h₀ : y₀ ∈ s<VAR>h₀i : MeasureTheory.Integrable (fun x => y₀) μ<GOAL>Filter.Tendsto (fun n => MeasureTheory.SimpleFunc.integral μ (MeasureTheory.SimpleFunc.approxOn f hfm s y₀ h₀ n)) Filter.atTop (𝓝 (∫ (x : α), f x ∂μ))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>f : α → E<VAR>fmeas : Measurable f<VAR>hf : MeasureTheory.Integrable f μ<VAR>s : Set E<VAR>TopologicalSpace.SeparableSpace ↑s<VAR>hs : Set.range f ∪ {0} ⊆ s<GOAL>Filter.Tendsto (fun n => MeasureTheory.SimpleFunc.integral μ (MeasureTheory.SimpleFunc.approxOn f fmeas s 0 ⋯ n)) Filter.atTop (𝓝 (∫ (x : α), f x ∂μ))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>f : α → E<VAR>fmeas : Measurable f<VAR>hf : MeasureTheory.Integrable f μ<VAR>TopologicalSpace.SeparableSpace ↑(Set.range f ∪ {0})<GOAL>Filter.Tendsto (fun n => ∫ (x : α), ‖↑(MeasureTheory.SimpleFunc.approxOn f fmeas (Set.range f ∪ {0}) 0 ⋯ n) x - f x‖ ∂μ) Filter.atTop (𝓝 0)
<VAR>α : Type u_1<VAR>G : Type u_5<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>f : α → G<VAR>hμ : MeasureTheory.Integrable f μ<VAR>hν : MeasureTheory.Integrable f ν<GOAL>∫ (x : α), f x ∂(μ + ν) = ∫ (x : α), f x ∂μ + ∫ (x : α), f x ∂ν
<VAR>α : Type u_1<VAR>G : Type u_5<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>m : MeasurableSpace α<VAR>f : α → G<GOAL>∫ (x : α), f x ∂0 = 0
<VAR>α : Type u_1<VAR>G : Type u_5<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>ι : Type u_7<VAR>m : MeasurableSpace α<VAR>f : α → G<VAR>μ : ι → MeasureTheory.Measure α<VAR>s : Finset ι<VAR>hf : ∀ i ∈ s, MeasureTheory.Integrable f (μ i)<GOAL>∫ (a : α), f a ∂∑ i ∈ s, μ i = ∑ i ∈ s, ∫ (a : α), f a ∂μ i
<VAR>α : Type u_1<VAR>G : Type u_5<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>f : α → G<VAR>h₁ : MeasureTheory.Integrable f μ<VAR>h₂ : MeasureTheory.Integrable f ν<GOAL>↑(nndist (∫ (x : α), f x ∂μ) (∫ (x : α), f x ∂(μ + ν))) ≤ ∫⁻ (x : α), ↑‖f x‖₊ ∂ν
<VAR>α : Type u_1<VAR>G : Type u_5<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>ι : Type u_7<VAR>m : MeasurableSpace α<VAR>f : α → G<VAR>μ : ι → MeasureTheory.Measure α<VAR>hf : MeasureTheory.Integrable f (MeasureTheory.Measure.sum μ)<GOAL>HasSum (fun i => ∫ (a : α), f a ∂μ i) (∫ (a : α), f a ∂MeasureTheory.Measure.sum μ)
<VAR>α : Type u_1<VAR>G : Type u_5<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>ι : Type u_7<GOAL>∀ {x : MeasurableSpace α} {f : α → G} {μ : ι → MeasureTheory.Measure α}, MeasureTheory.Integrable f (MeasureTheory.Measure.sum μ) → ∫ (a : α), f a ∂MeasureTheory.Measure.sum μ = ∑' (i : ι), ∫ (a : α), f a ∂μ i
<VAR>α : Type u_1<VAR>G : Type u_5<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → G<VAR>c : ℝ≥0∞<GOAL>∫ (x : α), f x ∂c • μ = c.toReal • ∫ (x : α), f x ∂μ
<VAR>α : Type u_1<VAR>G : Type u_5<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → G<VAR>c : ℝ≥0<GOAL>∫ (x : α), f x ∂c • μ = c • ∫ (x : α), f x ∂μ
<VAR>α : Type u_1<VAR>G : Type u_5<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>β : Type u_7<VAR>MeasurableSpace β<VAR>φ : α → β<VAR>hφ : Measurable φ<VAR>f : β → G<VAR>hfm : MeasureTheory.StronglyMeasurable f<GOAL>∫ (y : β), f y ∂MeasureTheory.Measure.map φ μ = ∫ (x : α), f (φ x) ∂μ
<VAR>α : Type u_1<VAR>G : Type u_5<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>β : Type u_7<VAR>MeasurableSpace β<VAR>φ : α → β<VAR>hφ : AEMeasurable φ μ<VAR>f : β → G<VAR>hfm : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.map φ μ)<GOAL>∫ (y : β), f y ∂MeasureTheory.Measure.map φ μ = ∫ (x : α), f (φ x) ∂μ
<VAR>α : Type u_1<VAR>G : Type u_5<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>β : Type u_7<GOAL>∀ {x : MeasurableSpace β} {f : α → β}, MeasurableEmbedding f → ∀ (g : β → G), ∫ (y : β), g y ∂MeasureTheory.Measure.map f μ = ∫ (x : α), g (f x) ∂μ
<VAR>α : Type u_1<VAR>G : Type u_5<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>β : Type u_7<VAR>TopologicalSpace α<VAR>BorelSpace α<VAR>TopologicalSpace β<VAR>MeasurableSpace β<VAR>BorelSpace β<VAR>φ : α → β<VAR>hφ : ClosedEmbedding φ<VAR>f : β → G<GOAL>∫ (y : β), f y ∂MeasureTheory.Measure.map φ μ = ∫ (x : α), f (φ x) ∂μ
<VAR>α : Type u_1<VAR>G : Type u_5<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>β : Type u_7<VAR>MeasurableSpace β<VAR>e : α ≃ᵐ β<VAR>f : β → G<GOAL>∫ (y : β), f y ∂MeasureTheory.Measure.map (⇑e) μ = ∫ (x : α), f (e x) ∂μ
<VAR>α : Type u_1<VAR>G : Type u_5<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>β : Type u_7<GOAL>∀ {x : MeasurableSpace β} {f : α → β} {ν : MeasureTheory.Measure β}, MeasureTheory.MeasurePreserving f μ ν → MeasurableEmbedding f → ∀ (g : β → G), ∫ (x : α), g (f x) ∂μ = ∫ (y : β), g y ∂ν
<VAR>α : Type u_1<VAR>G : Type u_5<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>β : Type u_7<VAR>MeasurableSpace β<VAR>ν : MeasureTheory.Measure β<VAR>f : α ≃ᵐ β<VAR>h : MeasureTheory.MeasurePreserving (⇑f) μ ν<VAR>g : β → G<GOAL>∫ (x : α), g (f x) ∂μ = ∫ (y : β), g y ∂ν
<VAR>G : Type u_5<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>α : Type u_7<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>f : α → G<GOAL>∫ (x : ↑s), f ↑x ∂MeasureTheory.Measure.comap Subtype.val μ = ∫ (x : α) in s, f x ∂μ
<VAR>G : Type u_5<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>α : Type u_7<VAR>MeasureTheory.MeasureSpace α<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>f : α → G<GOAL>∫ (x : ↑s), f ↑x = ∫ (x : α) in s, f x
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>MeasurableSpace α<VAR>f : α → E<VAR>a : α<VAR>hfm : MeasureTheory.StronglyMeasurable f<GOAL>∫ (x : α), f x ∂MeasureTheory.Measure.dirac a = f a
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>MeasurableSpace α<VAR>MeasurableSingletonClass α<VAR>f : α → E<VAR>a : α<GOAL>∫ (x : α), f x ∂MeasureTheory.Measure.dirac a = f a
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>mα : MeasurableSpace α<VAR>f : α → E<VAR>hf : MeasureTheory.StronglyMeasurable f<VAR>a : α<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>Decidable (a ∈ s)<GOAL>∫ (x : α) in s, f x ∂MeasureTheory.Measure.dirac a = if a ∈ s then f a else 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>MeasurableSpace α<VAR>MeasurableSingletonClass α<VAR>f : α → E<VAR>a : α<VAR>s : Set α<VAR>Decidable (a ∈ s)<GOAL>∫ (x : α) in s, f x ∂MeasureTheory.Measure.dirac a = if a ∈ s then f a else 0
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ<VAR>hf_nonneg : 0 ≤ᵐ[μ] f<VAR>hf_int : MeasureTheory.Integrable f μ<VAR>ε : ℝ<GOAL>ε * (μ {x | ε ≤ f x}).toReal ≤ ∫ (x : α), f x ∂μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>E : Type u_7<VAR>NormedAddCommGroup E<VAR>f g : α → E<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<VAR>hf : MeasureTheory.Memℒp f (ENNReal.ofReal p) μ<VAR>hg : MeasureTheory.Memℒp g (ENNReal.ofReal q) μ<GOAL>∫ (a : α), ‖f a‖ * ‖g a‖ ∂μ ≤ (∫ (a : α), ‖f a‖ ^ p ∂μ) ^ (1 / p) * (∫ (a : α), ‖g a‖ ^ q ∂μ) ^ (1 / q)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<VAR>f g : α → ℝ<VAR>hf_nonneg : 0 ≤ᵐ[μ] f<VAR>hg_nonneg : 0 ≤ᵐ[μ] g<VAR>hf : MeasureTheory.Memℒp f (ENNReal.ofReal p) μ<VAR>hg : MeasureTheory.Memℒp g (ENNReal.ofReal q) μ<GOAL>∫ (a : α), f a * g a ∂μ ≤ (∫ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫ (a : α), g a ^ q ∂μ) ^ (1 / q)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>m : MeasurableSpace α<VAR>Countable α<VAR>MeasurableSingletonClass α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → E<VAR>hf : MeasureTheory.Integrable f μ<GOAL>∫ (a : α), f a ∂μ = ∑' (a : α), (μ {a}).toReal • f a
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → E<VAR>hf : MeasureTheory.StronglyMeasurable f<VAR>a : α<GOAL>∫ (a : α) in {a}, f a ∂μ = (μ {a}).toReal • f a
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>m : MeasurableSpace α<VAR>MeasurableSingletonClass α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → E<VAR>a : α<GOAL>∫ (a : α) in {a}, f a ∂μ = (μ {a}).toReal • f a
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableSingletonClass α<VAR>f : α → E<VAR>s : Set α<VAR>hs : s.Countable<VAR>hf : MeasureTheory.Integrable f (μ.restrict s)<GOAL>∫ (a : α) in s, f a ∂μ = ∑' (a : ↑s), (μ {↑a}).toReal • f ↑a
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableSingletonClass α<VAR>s : Finset α<VAR>f : α → E<VAR>hf : MeasureTheory.Integrable f (μ.restrict ↑s)<GOAL>∫ (x : α) in ↑s, f x ∂μ = ∑ x ∈ s, (μ {x}).toReal • f x
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableSingletonClass α<VAR>Fintype α<VAR>f : α → E<VAR>hf : MeasureTheory.Integrable f μ<GOAL>∫ (x : α), f x ∂μ = ∑ x : α, (μ {x}).toReal • f x
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>Unique α<VAR>f : α → E<GOAL>∫ (x : α), f x ∂μ = (μ Set.univ).toReal • f default
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace α<VAR>μ.IsOpenPosMeasure<VAR>f : α → ℝ<VAR>x : α<VAR>f_cont : Continuous f<VAR>f_int : MeasureTheory.Integrable f μ<VAR>f_nonneg : 0 ≤ f<VAR>f_x : f x ≠ 0<GOAL>0 < ∫ (x : α), f x ∂μ
<VAR>β : Type u_7<VAR>γ : Type u_8<VAR>m m0 : MeasurableSpace β<VAR>hm : m ≤ m0<VAR>f : MeasureTheory.SimpleFunc β γ<GOAL>↑(MeasureTheory.SimpleFunc.toLargerSpace hm f) = ↑f
<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>CompleteSpace F<VAR>β : Type u_7<VAR>m m0 : MeasurableSpace β<VAR>μ : MeasureTheory.Measure β<VAR>hm : m ≤ m0<VAR>f : MeasureTheory.SimpleFunc β F<VAR>hf_int : MeasureTheory.Integrable (↑f) μ<GOAL>∫ (x : β), ↑f x ∂μ = ∑ x ∈ f.range, (μ (↑f ⁻¹' {x})).toReal • x
<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>CompleteSpace F<VAR>β : Type u_7<VAR>m m0 : MeasurableSpace β<VAR>μ : MeasureTheory.Measure β<VAR>hm : m ≤ m0<VAR>f : MeasureTheory.SimpleFunc β F<VAR>hf_int : MeasureTheory.Integrable (↑f) μ<GOAL>∫ (x : β), ↑f x ∂μ = ∫ (x : β), ↑f x ∂μ.trim hm
<VAR>G : Type u_5<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>β : Type u_7<VAR>m m0 : MeasurableSpace β<VAR>μ : MeasureTheory.Measure β<VAR>hm : m ≤ m0<VAR>f : β → G<VAR>hf : MeasureTheory.StronglyMeasurable f<GOAL>∫ (x : β), f x ∂μ = ∫ (x : β), f x ∂μ.trim hm
<VAR>G : Type u_5<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>β : Type u_7<VAR>m m0 : MeasurableSpace β<VAR>μ : MeasureTheory.Measure β<VAR>hm : m ≤ m0<VAR>f : β → G<VAR>hf : MeasureTheory.AEStronglyMeasurable f (μ.trim hm)<GOAL>∫ (x : β), f x ∂μ = ∫ (x : β), f x ∂μ.trim hm
<VAR>β : Type u_7<VAR>γ : Type u_8<VAR>m m0 : MeasurableSpace β<VAR>μ : MeasureTheory.Measure β<VAR>TopologicalSpace γ<VAR>TopologicalSpace.MetrizableSpace γ<VAR>hm : m ≤ m0<VAR>f g : β → γ<VAR>hf : MeasureTheory.StronglyMeasurable f<VAR>hg : MeasureTheory.StronglyMeasurable g<VAR>hfg : f =ᵐ[μ] g<GOAL>f =ᵐ[μ.trim hm] g
<VAR>β : Type u_7<VAR>γ : Type u_8<VAR>m m0 : MeasurableSpace β<VAR>μ : MeasureTheory.Measure β<VAR>TopologicalSpace γ<VAR>TopologicalSpace.MetrizableSpace γ<VAR>hm : m ≤ m0<VAR>f g : β → γ<VAR>hf : MeasureTheory.StronglyMeasurable f<VAR>hg : MeasureTheory.StronglyMeasurable g<GOAL>f =ᵐ[μ.trim hm] g ↔ f =ᵐ[μ] g
<VAR>β : Type u_7<VAR>γ : Type u_8<VAR>m m0 : MeasurableSpace β<VAR>μ : MeasureTheory.Measure β<VAR>LinearOrder γ<VAR>TopologicalSpace γ<VAR>OrderClosedTopology γ<VAR>TopologicalSpace.PseudoMetrizableSpace γ<VAR>hm : m ≤ m0<VAR>f g : β → γ<VAR>hf : MeasureTheory.StronglyMeasurable f<VAR>hg : MeasureTheory.StronglyMeasurable g<VAR>hfg : f ≤ᵐ[μ] g<GOAL>f ≤ᵐ[μ.trim hm] g
<VAR>β : Type u_7<VAR>γ : Type u_8<VAR>m m0 : MeasurableSpace β<VAR>μ : MeasureTheory.Measure β<VAR>LinearOrder γ<VAR>TopologicalSpace γ<VAR>OrderClosedTopology γ<VAR>TopologicalSpace.PseudoMetrizableSpace γ<VAR>hm : m ≤ m0<VAR>f g : β → γ<VAR>hf : MeasureTheory.StronglyMeasurable f<VAR>hg : MeasureTheory.StronglyMeasurable g<GOAL>f ≤ᵐ[μ.trim hm] g ↔ f ≤ᵐ[μ] g
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ<VAR>r : ℝ≥0<VAR>hfint : MeasureTheory.Integrable f μ<VAR>hfint' : 0 ≤ ∫ (x : α), f x ∂μ<VAR>hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r<GOAL>MeasureTheory.eLpNorm f 1 μ ≤ 2 * μ Set.univ * ↑r
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ<VAR>r : ℝ<VAR>hfint : MeasureTheory.Integrable f μ<VAR>hfint' : 0 ≤ ∫ (x : α), f x ∂μ<VAR>hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ r<GOAL>MeasureTheory.eLpNorm f 1 μ ≤ 2 * μ Set.univ * ENNReal.ofReal r
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>I J : BoxIntegral.Box ι<GOAL>J ∈ BoxIntegral.Prepartition.splitCenter I ↔ ∃ s, I.splitCenterBox s = J
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>I : BoxIntegral.Box ι<GOAL>(BoxIntegral.Prepartition.splitCenter I).IsPartition
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>I J : BoxIntegral.Box ι<VAR>h : J ∈ BoxIntegral.Prepartition.splitCenter I<VAR>i : ι<GOAL>J.upper i - J.lower i = (I.upper i - I.lower i) / 2
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>p : BoxIntegral.Box ι → Prop<VAR>I : BoxIntegral.Box ι<VAR>H_ind : ∀ J ≤ I, (∀ J' ∈ BoxIntegral.Prepartition.splitCenter J, p J') → p J<VAR>H_nhds : ∀ z ∈ BoxIntegral.Box.Icc I, ∃ U ∈ nhdsWithin z (BoxIntegral.Box.Icc I), ∀ J ≤ I, ∀ (m : ℕ), z ∈ BoxIntegral.Box.Icc J → BoxIntegral.Box.Icc J ⊆ U → (∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / 2 ^ m) → p J<GOAL>p I
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>I : BoxIntegral.Box ι<VAR>r : (ι → ℝ) → ↑(Set.Ioi 0)<GOAL>∃ π, π.IsPartition ∧ π.IsHenstock ∧ π.IsSubordinate r ∧ (∀ J ∈ π, ∃ m, ∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / 2 ^ m) ∧ π.distortion = I.distortion
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>I : BoxIntegral.Box ι<VAR>r : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>π : BoxIntegral.Prepartition I<GOAL>∃ π', π'.toPrepartition ≤ π ∧ π'.IsHenstock ∧ π'.IsSubordinate r ∧ π'.distortion = π.distortion ∧ π'.iUnion = π.iUnion
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>I : BoxIntegral.Box ι<VAR>π : BoxIntegral.Prepartition I<VAR>r : (ι → ℝ) → ↑(Set.Ioi 0)<GOAL>(π.toSubordinate r).toPrepartition ≤ π
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>I : BoxIntegral.Box ι<VAR>π : BoxIntegral.Prepartition I<VAR>r : (ι → ℝ) → ↑(Set.Ioi 0)<GOAL>(π.toSubordinate r).IsHenstock
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>I : BoxIntegral.Box ι<VAR>π : BoxIntegral.Prepartition I<VAR>r : (ι → ℝ) → ↑(Set.Ioi 0)<GOAL>(π.toSubordinate r).IsSubordinate r
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>I : BoxIntegral.Box ι<VAR>π : BoxIntegral.Prepartition I<VAR>r : (ι → ℝ) → ↑(Set.Ioi 0)<GOAL>(π.toSubordinate r).distortion = π.distortion
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>I : BoxIntegral.Box ι<VAR>π : BoxIntegral.Prepartition I<VAR>r : (ι → ℝ) → ↑(Set.Ioi 0)<GOAL>(π.toSubordinate r).iUnion = π.iUnion
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>I : BoxIntegral.Box ι<VAR>π₁ : BoxIntegral.TaggedPrepartition I<VAR>π₂ : BoxIntegral.Prepartition I<VAR>hU : π₂.iUnion = ↑I \ π₁.iUnion<VAR>r : (ι → ℝ) → ↑(Set.Ioi 0)<GOAL>(π₁.unionComplToSubordinate π₂ hU r).IsPartition
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>I : BoxIntegral.Box ι<VAR>π₁ : BoxIntegral.TaggedPrepartition I<VAR>π₂ : BoxIntegral.Prepartition I<VAR>hU : π₂.iUnion = ↑I \ π₁.iUnion<VAR>r : (ι → ℝ) → ↑(Set.Ioi 0)<GOAL>(π₁.unionComplToSubordinate π₂ hU r).boxes = π₁.boxes ∪ (π₂.toSubordinate r).boxes
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>I : BoxIntegral.Box ι<VAR>π₁ : BoxIntegral.TaggedPrepartition I<VAR>π₂ : BoxIntegral.Prepartition I<VAR>hU : π₂.iUnion = ↑I \ π₁.iUnion<VAR>r : (ι → ℝ) → ↑(Set.Ioi 0)<GOAL>(π₁.unionComplToSubordinate π₂ hU r).iUnion = ↑I
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>I : BoxIntegral.Box ι<VAR>π₁ : BoxIntegral.TaggedPrepartition I<VAR>π₂ : BoxIntegral.Prepartition I<VAR>hU : π₂.iUnion = ↑I \ π₁.iUnion<VAR>r : (ι → ℝ) → ↑(Set.Ioi 0)<GOAL>(π₁.unionComplToSubordinate π₂ hU r).distortion = max π₁.distortion π₂.distortion
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>self : BoxIntegral.TaggedPrepartition I<VAR>J : BoxIntegral.Box ι<GOAL>self.tag J ∈ BoxIntegral.Box.Icc I
<VAR>ι : Type u_1<VAR>I J : BoxIntegral.Box ι<VAR>π : BoxIntegral.TaggedPrepartition I<GOAL>J ∈ π.toPrepartition ↔ J ∈ π
<VAR>ι : Type u_1<VAR>I J : BoxIntegral.Box ι<VAR>π : BoxIntegral.Prepartition I<VAR>f : BoxIntegral.Box ι → ι → ℝ<VAR>h : ∀ (J : BoxIntegral.Box ι), f J ∈ BoxIntegral.Box.Icc I<GOAL>J ∈ { toPrepartition := π, tag := f, tag_mem_Icc := h } ↔ J ∈ π
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>π : BoxIntegral.TaggedPrepartition I<GOAL>π.iUnion = ⋃ J ∈ π, ↑J
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>π : BoxIntegral.Prepartition I<VAR>f : BoxIntegral.Box ι → ι → ℝ<VAR>h : ∀ (J : BoxIntegral.Box ι), f J ∈ BoxIntegral.Box.Icc I<GOAL>{ toPrepartition := π, tag := f, tag_mem_Icc := h }.iUnion = π.iUnion
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>π : BoxIntegral.TaggedPrepartition I<GOAL>π.iUnion = π.iUnion
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>π : BoxIntegral.TaggedPrepartition I<VAR>x : ι → ℝ<GOAL>x ∈ π.iUnion ↔ ∃ J ∈ π, x ∈ J
<VAR>ι : Type u_1<VAR>I J : BoxIntegral.Box ι<VAR>π : BoxIntegral.TaggedPrepartition I<VAR>h : J ∈ π<GOAL>↑J ⊆ π.iUnion
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>π : BoxIntegral.TaggedPrepartition I<GOAL>π.iUnion ⊆ ↑I
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>π : BoxIntegral.TaggedPrepartition I<GOAL>π.IsPartition ↔ π.iUnion = ↑I
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>π : BoxIntegral.TaggedPrepartition I<VAR>p : BoxIntegral.Box ι → Prop<GOAL>(π.filter p).boxes.val = Multiset.filter p π.boxes.val
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>π : BoxIntegral.TaggedPrepartition I<VAR>p : BoxIntegral.Box ι → Prop<GOAL>(π.filter p).tag = π.tag
<VAR>ι : Type u_1<VAR>I J : BoxIntegral.Box ι<VAR>π : BoxIntegral.TaggedPrepartition I<VAR>p : BoxIntegral.Box ι → Prop<GOAL>J ∈ π.filter p ↔ J ∈ π ∧ p J
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>π : BoxIntegral.TaggedPrepartition I<VAR>p : BoxIntegral.Box ι → Prop<GOAL>(π.filter fun J => ¬p J).iUnion = π.iUnion \ (π.filter p).iUnion
<VAR>ι : Type u_1<VAR>I J : BoxIntegral.Box ι<VAR>π : BoxIntegral.Prepartition I<VAR>πi : (J : BoxIntegral.Box ι) → BoxIntegral.TaggedPrepartition J<GOAL>J ∈ π.biUnionTagged πi ↔ ∃ J' ∈ π, J ∈ πi J'
<VAR>ι : Type u_1<VAR>I J : BoxIntegral.Box ι<VAR>π : BoxIntegral.Prepartition I<VAR>πi : (J : BoxIntegral.Box ι) → BoxIntegral.TaggedPrepartition J<VAR>hJ : J ∈ π<VAR>J' : BoxIntegral.Box ι<VAR>hJ' : J' ∈ πi J<GOAL>(π.biUnionTagged πi).tag J' = (πi J).tag J'
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>π : BoxIntegral.Prepartition I<VAR>πi : (J : BoxIntegral.Box ι) → BoxIntegral.TaggedPrepartition J<GOAL>(π.biUnionTagged πi).iUnion = ⋃ J ∈ π, (πi J).iUnion
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>p : (ι → ℝ) → BoxIntegral.Box ι → Prop<VAR>π : BoxIntegral.Prepartition I<VAR>πi : (J : BoxIntegral.Box ι) → BoxIntegral.TaggedPrepartition J<GOAL>(∀ J ∈ π.biUnionTagged πi, p ((π.biUnionTagged πi).tag J) J) ↔ ∀ J ∈ π, ∀ J' ∈ πi J, p ((πi J).tag J') J'
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>π : BoxIntegral.Prepartition I<VAR>h : π.IsPartition<VAR>πi : (J : BoxIntegral.Box ι) → BoxIntegral.TaggedPrepartition J<VAR>hi : ∀ J ∈ π, (πi J).IsPartition<GOAL>(π.biUnionTagged πi).IsPartition
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>π : BoxIntegral.TaggedPrepartition I<VAR>πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J<GOAL>(π.biUnionPrepartition πi).tag = fun J => π.tag (π.biUnionIndex πi J)
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>π : BoxIntegral.TaggedPrepartition I<VAR>h : π.IsPartition<VAR>πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J<VAR>hi : ∀ J ∈ π, (πi J).IsPartition<GOAL>(π.biUnionPrepartition πi).IsPartition
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>π : BoxIntegral.TaggedPrepartition I<VAR>π' : BoxIntegral.Prepartition I<GOAL>(π.infPrepartition π').toPrepartition = π.toPrepartition ⊓ π'
<VAR>ι : Type u_1<VAR>I J : BoxIntegral.Box ι<VAR>π₁ π₂ : BoxIntegral.TaggedPrepartition I<GOAL>J ∈ π₁.infPrepartition π₂.toPrepartition ↔ J ∈ π₂.infPrepartition π₁.toPrepartition
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>π₁ : BoxIntegral.TaggedPrepartition I<VAR>h₁ : π₁.IsPartition<VAR>π₂ : BoxIntegral.Prepartition I<VAR>h₂ : π₂.IsPartition<GOAL>(π₁.infPrepartition π₂).IsPartition
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>π : BoxIntegral.Prepartition I<VAR>πi : (J : BoxIntegral.Box ι) → BoxIntegral.TaggedPrepartition J<GOAL>(π.biUnionTagged πi).IsHenstock ↔ ∀ J ∈ π, (πi J).IsHenstock
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>π : BoxIntegral.TaggedPrepartition I<VAR>Fintype ι<VAR>h : π.IsHenstock<VAR>x : ι → ℝ<GOAL>(Finset.filter (fun J => π.tag J = x) π.boxes).card ≤ 2 ^ Fintype.card ι
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>r : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>Fintype ι<VAR>π : BoxIntegral.Prepartition I<VAR>πi : (J : BoxIntegral.Box ι) → BoxIntegral.TaggedPrepartition J<GOAL>(π.biUnionTagged πi).IsSubordinate r ↔ ∀ J ∈ π, (πi J).IsSubordinate r
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>π : BoxIntegral.TaggedPrepartition I<VAR>r : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>Fintype ι<VAR>h : π.IsSubordinate r<VAR>πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J<GOAL>(π.biUnionPrepartition πi).IsSubordinate r
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>π : BoxIntegral.TaggedPrepartition I<VAR>r : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>Fintype ι<VAR>h : π.IsSubordinate r<VAR>π' : BoxIntegral.Prepartition I<GOAL>(π.infPrepartition π').IsSubordinate r
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>Fintype ι<VAR>π : BoxIntegral.TaggedPrepartition I<VAR>hr₁ : π.IsSubordinate r₁<VAR>h : ∀ J ∈ π, r₁ (π.tag J) ≤ r₂ (π.tag J)<GOAL>π.IsSubordinate r₂