internlm/Lean-Github huggingface dataset:
Theorem: MeasureTheory.LocallyIntegrable.integrable_of_isBigO_atTop_of_norm_eq_norm_neg
Proof state before:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁹ : MeasurableSpace α
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
f : α → E
g : α → F
a✝ b : α
μ : Measure α
l : Filter α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : SecondCountableTopology α
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : CompactIccSpace α
inst✝² : atTop.IsMeasurablyGenerated
inst✝¹ : MeasurableNeg α
inst✝ : μ.IsNegInvariant
hf : LocallyIntegrable f μ
hsymm : norm ∘ f =ᶠ[ae μ] norm ∘ f ∘ Neg.neg
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
x✝ : Nonempty α
a : α := -|Classical.arbitrary α|
h_int : IntegrableOn f (Ici a) μ
h_map_neg : Measure.map Neg.neg (μ.restrict (Ici a)) = μ.restrict (Iic (-a))
⊢ Integrable f μ
Tactic:
have h_int_neg : IntegrableOn (f ∘ Neg.neg) (Ici a) μ := by
  refine h_int.congr' ?_ hsymm.restrict
  refine AEStronglyMeasurable.comp_aemeasurable ?_ measurable_neg.aemeasurable
  convert hf.aestronglyMeasurable.restrict
Proof state after:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁹ : MeasurableSpace α
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
f : α → E
g : α → F
a✝ b : α
μ : Measure α
l : Filter α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : SecondCountableTopology α
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : CompactIccSpace α
inst✝² : atTop.IsMeasurablyGenerated
inst✝¹ : MeasurableNeg α
inst✝ : μ.IsNegInvariant
hf : LocallyIntegrable f μ
hsymm : norm ∘ f =ᶠ[ae μ] norm ∘ f ∘ Neg.neg
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
x✝ : Nonempty α
a : α := -|Classical.arbitrary α|
h_int : IntegrableOn f (Ici a) μ
h_map_neg : Measure.map Neg.neg (μ.restrict (Ici a)) = μ.restrict (Iic (-a))
h_int_neg : IntegrableOn (f ∘ Neg.neg) (Ici a) μ
⊢ Integrable f μ
Theorem: MeasureTheory.LocallyIntegrable.integrable_of_isBigO_atTop_of_norm_eq_norm_neg
Proof state before:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁹ : MeasurableSpace α
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
f : α → E
g : α → F
a✝ b : α
μ : Measure α
l : Filter α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : SecondCountableTopology α
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : CompactIccSpace α
inst✝² : atTop.IsMeasurablyGenerated
inst✝¹ : MeasurableNeg α
inst✝ : μ.IsNegInvariant
hf : LocallyIntegrable f μ
hsymm : norm ∘ f =ᶠ[ae μ] norm ∘ f ∘ Neg.neg
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
x✝ : Nonempty α
a : α := -|Classical.arbitrary α|
h_int : IntegrableOn f (Ici a) μ
h_map_neg : Measure.map Neg.neg (μ.restrict (Ici a)) = μ.restrict (Iic (-a))
h_int_neg : IntegrableOn (f ∘ Neg.neg) (Ici a) μ
⊢ Integrable f μ
Tactic:
replace h_int_neg := measurableEmbedding_neg.integrable_map_iff.mpr h_int_neg
Proof state after:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁹ : MeasurableSpace α
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
f : α → E
g : α → F
a✝ b : α
μ : Measure α
l : Filter α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : SecondCountableTopology α
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : CompactIccSpace α
inst✝² : atTop.IsMeasurablyGenerated
inst✝¹ : MeasurableNeg α
inst✝ : μ.IsNegInvariant
hf : LocallyIntegrable f μ
hsymm : norm ∘ f =ᶠ[ae μ] norm ∘ f ∘ Neg.neg
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
x✝ : Nonempty α
a : α := -|Classical.arbitrary α|
h_int : IntegrableOn f (Ici a) μ
h_map_neg : Measure.map Neg.neg (μ.restrict (Ici a)) = μ.restrict (Iic (-a))
h_int_neg : Integrable f (Measure.map Neg.neg (μ.restrict (Ici a)))
⊢ Integrable f μ
Theorem: MeasureTheory.LocallyIntegrable.integrable_of_isBigO_atTop_of_norm_eq_norm_neg
Proof state before:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁹ : MeasurableSpace α
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
f : α → E
g : α → F
a✝ b : α
μ : Measure α
l : Filter α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : SecondCountableTopology α
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : CompactIccSpace α
inst✝² : atTop.IsMeasurablyGenerated
inst✝¹ : MeasurableNeg α
inst✝ : μ.IsNegInvariant
hf : LocallyIntegrable f μ
hsymm : norm ∘ f =ᶠ[ae μ] norm ∘ f ∘ Neg.neg
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
x✝ : Nonempty α
a : α := -|Classical.arbitrary α|
h_int : IntegrableOn f (Ici a) μ
h_map_neg : Measure.map Neg.neg (μ.restrict (Ici a)) = μ.restrict (Iic (-a))
h_int_neg : Integrable f (Measure.map Neg.neg (μ.restrict (Ici a)))
⊢ Integrable f μ
Tactic:
rewrite [h_map_neg] at h_int_neg
Proof state after:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁹ : MeasurableSpace α
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
f : α → E
g : α → F
a✝ b : α
μ : Measure α
l : Filter α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : SecondCountableTopology α
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : CompactIccSpace α
inst✝² : atTop.IsMeasurablyGenerated
inst✝¹ : MeasurableNeg α
inst✝ : μ.IsNegInvariant
hf : LocallyIntegrable f μ
hsymm : norm ∘ f =ᶠ[ae μ] norm ∘ f ∘ Neg.neg
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
x✝ : Nonempty α
a : α := -|Classical.arbitrary α|
h_int : IntegrableOn f (Ici a) μ
h_map_neg : Measure.map Neg.neg (μ.restrict (Ici a)) = μ.restrict (Iic (-a))
h_int_neg : Integrable f (μ.restrict (Iic (-a)))
⊢ Integrable f μ
Theorem: MeasureTheory.LocallyIntegrable.integrable_of_isBigO_atTop_of_norm_eq_norm_neg
Proof state before:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁹ : MeasurableSpace α
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
f : α → E
g : α → F
a✝ b : α
μ : Measure α
l : Filter α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : SecondCountableTopology α
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : CompactIccSpace α
inst✝² : atTop.IsMeasurablyGenerated
inst✝¹ : MeasurableNeg α
inst✝ : μ.IsNegInvariant
hf : LocallyIntegrable f μ
hsymm : norm ∘ f =ᶠ[ae μ] norm ∘ f ∘ Neg.neg
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
x✝ : Nonempty α
a : α := -|Classical.arbitrary α|
h_int : IntegrableOn f (Ici a) μ
h_map_neg : Measure.map Neg.neg (μ.restrict (Ici a)) = μ.restrict (Iic (-a))
h_int_neg : Integrable f (μ.restrict (Iic (-a)))
⊢ Integrable f μ
Tactic:
refine integrableOn_univ.mp ?_
Proof state after:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁹ : MeasurableSpace α
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
f : α → E
g : α → F
a✝ b : α
μ : Measure α
l : Filter α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : SecondCountableTopology α
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : CompactIccSpace α
inst✝² : atTop.IsMeasurablyGenerated
inst✝¹ : MeasurableNeg α
inst✝ : μ.IsNegInvariant
hf : LocallyIntegrable f μ
hsymm : norm ∘ f =ᶠ[ae μ] norm ∘ f ∘ Neg.neg
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
x✝ : Nonempty α
a : α := -|Classical.arbitrary α|
h_int : IntegrableOn f (Ici a) μ
h_map_neg : Measure.map Neg.neg (μ.restrict (Ici a)) = μ.restrict (Iic (-a))
h_int_neg : Integrable f (μ.restrict (Iic (-a)))
⊢ IntegrableOn f univ μ
Theorem: MeasureTheory.LocallyIntegrable.integrable_of_isBigO_atTop_of_norm_eq_norm_neg
Proof state before:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁹ : MeasurableSpace α
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
f : α → E
g : α → F
a✝ b : α
μ : Measure α
l : Filter α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : SecondCountableTopology α
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : CompactIccSpace α
inst✝² : atTop.IsMeasurablyGenerated
inst✝¹ : MeasurableNeg α
inst✝ : μ.IsNegInvariant
hf : LocallyIntegrable f μ
hsymm : norm ∘ f =ᶠ[ae μ] norm ∘ f ∘ Neg.neg
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
x✝ : Nonempty α
a : α := -|Classical.arbitrary α|
h_int : IntegrableOn f (Ici a) μ
h_map_neg : Measure.map Neg.neg (μ.restrict (Ici a)) = μ.restrict (Iic (-a))
h_int_neg : Integrable f (μ.restrict (Iic (-a)))
⊢ IntegrableOn f univ μ
Tactic:
convert integrableOn_union.mpr ⟨h_int_neg, h_int⟩
Proof state after:
case h.e'_6
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁹ : MeasurableSpace α
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
f : α → E
g : α → F
a✝ b : α
μ : Measure α
l : Filter α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : SecondCountableTopology α
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : CompactIccSpace α
inst✝² : atTop.IsMeasurablyGenerated
inst✝¹ : MeasurableNeg α
inst✝ : μ.IsNegInvariant
hf : LocallyIntegrable f μ
hsymm : norm ∘ f =ᶠ[ae μ] norm ∘ f ∘ Neg.neg
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
x✝ : Nonempty α
a : α := -|Classical.arbitrary α|
h_int : IntegrableOn f (Ici a) μ
h_map_neg : Measure.map Neg.neg (μ.restrict (Ici a)) = μ.restrict (Iic (-a))
h_int_neg : Integrable f (μ.restrict (Iic (-a)))
⊢ univ = Iic (-a) ∪ Ici a
Theorem: MeasureTheory.LocallyIntegrable.integrable_of_isBigO_atTop_of_norm_eq_norm_neg
Proof state before:
case h.e'_6
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁹ : MeasurableSpace α
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
f : α → E
g : α → F
a✝ b : α
μ : Measure α
l : Filter α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : SecondCountableTopology α
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : CompactIccSpace α
inst✝² : atTop.IsMeasurablyGenerated
inst✝¹ : MeasurableNeg α
inst✝ : μ.IsNegInvariant
hf : LocallyIntegrable f μ
hsymm : norm ∘ f =ᶠ[ae μ] norm ∘ f ∘ Neg.neg
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
x✝ : Nonempty α
a : α := -|Classical.arbitrary α|
h_int : IntegrableOn f (Ici a) μ
h_map_neg : Measure.map Neg.neg (μ.restrict (Ici a)) = μ.restrict (Iic (-a))
h_int_neg : Integrable f (μ.restrict (Iic (-a)))
⊢ univ = Iic (-a) ∪ Ici a
Tactic:
exact (Set.Iic_union_Ici_of_le (by simp [a])).symm
Proof state after:
no goals
Theorem: MeasureTheory.LocallyIntegrable.integrable_of_isBigO_atTop_of_norm_eq_norm_neg
Proof state before:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁹ : MeasurableSpace α
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
f : α → E
g : α → F
a✝ b : α
μ : Measure α
l : Filter α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : SecondCountableTopology α
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : CompactIccSpace α
inst✝² : atTop.IsMeasurablyGenerated
inst✝¹ : MeasurableNeg α
inst✝ : μ.IsNegInvariant
hf : LocallyIntegrable f μ
hsymm : norm ∘ f =ᶠ[ae μ] norm ∘ f ∘ Neg.neg
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
x✝ : Nonempty α
a : α := -|Classical.arbitrary α|
h_int : IntegrableOn f (Ici a) μ
⊢ Measure.map Neg.neg (μ.restrict (Ici a)) = μ.restrict (Iic (-a))
Tactic:
rw [show Ici a = Neg.neg ⁻¹' Iic (-a) by simp, ← measurableEmbedding_neg.restrict_map,
  Measure.map_neg_eq_self]
Proof state after:
no goals
Theorem: MeasureTheory.LocallyIntegrable.integrable_of_isBigO_atTop_of_norm_eq_norm_neg
Proof state before:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁹ : MeasurableSpace α
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
f : α → E
g : α → F
a✝ b : α
μ : Measure α
l : Filter α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : SecondCountableTopology α
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : CompactIccSpace α
inst✝² : atTop.IsMeasurablyGenerated
inst✝¹ : MeasurableNeg α
inst✝ : μ.IsNegInvariant
hf : LocallyIntegrable f μ
hsymm : norm ∘ f =ᶠ[ae μ] norm ∘ f ∘ Neg.neg
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
x✝ : Nonempty α
a : α := -|Classical.arbitrary α|
h_int : IntegrableOn f (Ici a) μ
⊢ Ici a = Neg.neg ⁻¹' Iic (-a)
Tactic:
simp
Proof state after:
no goals
Theorem: MeasureTheory.LocallyIntegrable.integrable_of_isBigO_atTop_of_norm_eq_norm_neg
Proof state before:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁹ : MeasurableSpace α
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
f : α → E
g : α → F
a✝ b : α
μ : Measure α
l : Filter α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : SecondCountableTopology α
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : CompactIccSpace α
inst✝² : atTop.IsMeasurablyGenerated
inst✝¹ : MeasurableNeg α
inst✝ : μ.IsNegInvariant
hf : LocallyIntegrable f μ
hsymm : norm ∘ f =ᶠ[ae μ] norm ∘ f ∘ Neg.neg
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
x✝ : Nonempty α
a : α := -|Classical.arbitrary α|
h_int : IntegrableOn f (Ici a) μ
h_map_neg : Measure.map Neg.neg (μ.restrict (Ici a)) = μ.restrict (Iic (-a))
⊢ IntegrableOn (f ∘ Neg.neg) (Ici a) μ
Tactic:
refine h_int.congr' ?_ hsymm.restrict
Proof state after:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁹ : MeasurableSpace α
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
f : α → E
g : α → F
a✝ b : α
μ : Measure α
l : Filter α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : SecondCountableTopology α
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : CompactIccSpace α
inst✝² : atTop.IsMeasurablyGenerated
inst✝¹ : MeasurableNeg α
inst✝ : μ.IsNegInvariant
hf : LocallyIntegrable f μ
hsymm : norm ∘ f =ᶠ[ae μ] norm ∘ f ∘ Neg.neg
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
x✝ : Nonempty α
a : α := -|Classical.arbitrary α|
h_int : IntegrableOn f (Ici a) μ
h_map_neg : Measure.map Neg.neg (μ.restrict (Ici a)) = μ.restrict (Iic (-a))
⊢ AEStronglyMeasurable (f ∘ Neg.neg) (μ.restrict (Ici a))
Theorem: MeasureTheory.LocallyIntegrable.integrable_of_isBigO_atTop_of_norm_eq_norm_neg
Proof state before:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁹ : MeasurableSpace α
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
f : α → E
g : α → F
a✝ b : α
μ : Measure α
l : Filter α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : SecondCountableTopology α
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : CompactIccSpace α
inst✝² : atTop.IsMeasurablyGenerated
inst✝¹ : MeasurableNeg α
inst✝ : μ.IsNegInvariant
hf : LocallyIntegrable f μ
hsymm : norm ∘ f =ᶠ[ae μ] norm ∘ f ∘ Neg.neg
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
x✝ : Nonempty α
a : α := -|Classical.arbitrary α|
h_int : IntegrableOn f (Ici a) μ
h_map_neg : Measure.map Neg.neg (μ.restrict (Ici a)) = μ.restrict (Iic (-a))
⊢ AEStronglyMeasurable (f ∘ Neg.neg) (μ.restrict (Ici a))
Tactic:
refine AEStronglyMeasurable.comp_aemeasurable ?_ measurable_neg.aemeasurable
Proof state after:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁹ : MeasurableSpace α
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
f : α → E
g : α → F
a✝ b : α
μ : Measure α
l : Filter α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : SecondCountableTopology α
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : CompactIccSpace α
inst✝² : atTop.IsMeasurablyGenerated
inst✝¹ : MeasurableNeg α
inst✝ : μ.IsNegInvariant
hf : LocallyIntegrable f μ
hsymm : norm ∘ f =ᶠ[ae μ] norm ∘ f ∘ Neg.neg
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
x✝ : Nonempty α
a : α := -|Classical.arbitrary α|
h_int : IntegrableOn f (Ici a) μ
h_map_neg : Measure.map Neg.neg (μ.restrict (Ici a)) = μ.restrict (Iic (-a))
⊢ AEStronglyMeasurable f (Measure.map Neg.neg (μ.restrict (Ici a)))
Theorem: MeasureTheory.LocallyIntegrable.integrable_of_isBigO_atTop_of_norm_eq_norm_neg
Proof state before:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁹ : MeasurableSpace α
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
f : α → E
g : α → F
a✝ b : α
μ : Measure α
l : Filter α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : SecondCountableTopology α
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : CompactIccSpace α
inst✝² : atTop.IsMeasurablyGenerated
inst✝¹ : MeasurableNeg α
inst✝ : μ.IsNegInvariant
hf : LocallyIntegrable f μ
hsymm : norm ∘ f =ᶠ[ae μ] norm ∘ f ∘ Neg.neg
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
x✝ : Nonempty α
a : α := -|Classical.arbitrary α|
h_int : IntegrableOn f (Ici a) μ
h_map_neg : Measure.map Neg.neg (μ.restrict (Ici a)) = μ.restrict (Iic (-a))
⊢ AEStronglyMeasurable f (Measure.map Neg.neg (μ.restrict (Ici a)))
Tactic:
convert hf.aestronglyMeasurable.restrict
Proof state after:
no goals
Theorem: MeasureTheory.LocallyIntegrable.integrable_of_isBigO_atTop_of_norm_eq_norm_neg
Proof state before:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁹ : MeasurableSpace α
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
f : α → E
g : α → F
a✝ b : α
μ : Measure α
l : Filter α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : SecondCountableTopology α
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : CompactIccSpace α
inst✝² : atTop.IsMeasurablyGenerated
inst✝¹ : MeasurableNeg α
inst✝ : μ.IsNegInvariant
hf : LocallyIntegrable f μ
hsymm : norm ∘ f =ᶠ[ae μ] norm ∘ f ∘ Neg.neg
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
x✝ : Nonempty α
a : α := -|Classical.arbitrary α|
h_int : IntegrableOn f (Ici a) μ
h_map_neg : Measure.map Neg.neg (μ.restrict (Ici a)) = μ.restrict (Iic (-a))
h_int_neg : Integrable f (μ.restrict (Iic (-a)))
⊢ a ≤ -a
Tactic:
simp [a]
Proof state after:
no goals
Theorem: MeasureTheory.Asymptotics.IsBigO.eventually_integrableOn
Proof state before:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
f✝ : α → E
g : α → F
a b : α
μ✝ : Measure α
l : Filter α
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
ι : Type u_4
inst✝¹ : MeasurableSpace ι
f : ι × α → E
s : Set ι
μ : Measure ι
inst✝ : Norm F
hf :
  f =O[𝓟 s ×ˢ l] fun x =>
    match x with
    | (_i, x) => g x
hfm : ∀ᶠ (x : α) in l, AEStronglyMeasurable (fun i => f (i, x)) (μ.restrict s)
hs : MeasurableSet s
hμ : μ s < ⊤
⊢ ∀ᶠ (x : α) in l, IntegrableOn (fun i => f (i, x)) s μ
Tactic:
obtain ⟨C, hC⟩ := hf.bound
Proof state after:
case intro
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
f✝ : α → E
g : α → F
a b : α
μ✝ : Measure α
l : Filter α
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
ι : Type u_4
inst✝¹ : MeasurableSpace ι
f : ι × α → E
s : Set ι
μ : Measure ι
inst✝ : Norm F
hf :
  f =O[𝓟 s ×ˢ l] fun x =>
    match x with
    | (_i, x) => g x
hfm : ∀ᶠ (x : α) in l, AEStronglyMeasurable (fun i => f (i, x)) (μ.restrict s)
hs : MeasurableSet s
hμ : μ s < ⊤
C : ℝ
hC :
  ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l,
    ‖f x‖ ≤
      C *
        ‖match x with
          | (_i, x) => g x‖
⊢ ∀ᶠ (x : α) in l, IntegrableOn (fun i => f (i, x)) s μ
Theorem: MeasureTheory.Asymptotics.IsBigO.eventually_integrableOn
Proof state before:
case intro
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
f✝ : α → E
g : α → F
a b : α
μ✝ : Measure α
l : Filter α
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
ι : Type u_4
inst✝¹ : MeasurableSpace ι
f : ι × α → E
s : Set ι
μ : Measure ι
inst✝ : Norm F
hf :
  f =O[𝓟 s ×ˢ l] fun x =>
    match x with
    | (_i, x) => g x
hfm : ∀ᶠ (x : α) in l, AEStronglyMeasurable (fun i => f (i, x)) (μ.restrict s)
hs : MeasurableSet s
hμ : μ s < ⊤
C : ℝ
hC :
  ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l,
    ‖f x‖ ≤
      C *
        ‖match x with
          | (_i, x) => g x‖
⊢ ∀ᶠ (x : α) in l, IntegrableOn (fun i => f (i, x)) s μ
Tactic:
obtain ⟨t, htl, ht⟩ := hC.exists_mem
Proof state after:
case intro.intro.intro
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
f✝ : α → E
g : α → F
a b : α
μ✝ : Measure α
l : Filter α
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
ι : Type u_4
inst✝¹ : MeasurableSpace ι
f : ι × α → E
s : Set ι
μ : Measure ι
inst✝ : Norm F
hf :
  f =O[𝓟 s ×ˢ l] fun x =>
    match x with
    | (_i, x) => g x
hfm : ∀ᶠ (x : α) in l, AEStronglyMeasurable (fun i => f (i, x)) (μ.restrict s)
hs : MeasurableSet s
hμ : μ s < ⊤
C : ℝ
hC :
  ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l,
    ‖f x‖ ≤
      C *
        ‖match x with
          | (_i, x) => g x‖
t : Set (ι × α)
htl : t ∈ 𝓟 s ×ˢ l
ht :
  ∀ y ∈ t,
    ‖f y‖ ≤
      C *
        ‖match y with
          | (_i, x) => g x‖
⊢ ∀ᶠ (x : α) in l, IntegrableOn (fun i => f (i, x)) s μ
Theorem: MeasureTheory.Asymptotics.IsBigO.eventually_integrableOn
Proof state before:
case intro.intro.intro
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
f✝ : α → E
g : α → F
a b : α
μ✝ : Measure α
l : Filter α
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
ι : Type u_4
inst✝¹ : MeasurableSpace ι
f : ι × α → E
s : Set ι
μ : Measure ι
inst✝ : Norm F
hf :
  f =O[𝓟 s ×ˢ l] fun x =>
    match x with
    | (_i, x) => g x
hfm : ∀ᶠ (x : α) in l, AEStronglyMeasurable (fun i => f (i, x)) (μ.restrict s)
hs : MeasurableSet s
hμ : μ s < ⊤
C : ℝ
hC :
  ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l,
    ‖f x‖ ≤
      C *
        ‖match x with
          | (_i, x) => g x‖
t : Set (ι × α)
htl : t ∈ 𝓟 s ×ˢ l
ht :
  ∀ y ∈ t,
    ‖f y‖ ≤
      C *
        ‖match y with
          | (_i, x) => g x‖
⊢ ∀ᶠ (x : α) in l, IntegrableOn (fun i => f (i, x)) s μ
Tactic:
obtain ⟨u, hu, v, hv, huv⟩ := Filter.mem_prod_iff.mp htl
Proof state after:
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
f✝ : α → E
g : α → F
a b : α
μ✝ : Measure α
l : Filter α
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
ι : Type u_4
inst✝¹ : MeasurableSpace ι
f : ι × α → E
s : Set ι
μ : Measure ι
inst✝ : Norm F
hf :
  f =O[𝓟 s ×ˢ l] fun x =>
    match x with
    | (_i, x) => g x
hfm : ∀ᶠ (x : α) in l, AEStronglyMeasurable (fun i => f (i, x)) (μ.restrict s)
hs : MeasurableSet s
hμ : μ s < ⊤
C : ℝ
hC :
  ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l,
    ‖f x‖ ≤
      C *
        ‖match x with
          | (_i, x) => g x‖
t : Set (ι × α)
htl : t ∈ 𝓟 s ×ˢ l
ht :
  ∀ y ∈ t,
    ‖f y‖ ≤
      C *
        ‖match y with
          | (_i, x) => g x‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
⊢ ∀ᶠ (x : α) in l, IntegrableOn (fun i => f (i, x)) s μ
Theorem: MeasureTheory.Asymptotics.IsBigO.eventually_integrableOn
Proof state before:
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
f✝ : α → E
g : α → F
a b : α
μ✝ : Measure α
l : Filter α
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
ι : Type u_4
inst✝¹ : MeasurableSpace ι
f : ι × α → E
s : Set ι
μ : Measure ι
inst✝ : Norm F
hf :
  f =O[𝓟 s ×ˢ l] fun x =>
    match x with
    | (_i, x) => g x
hfm : ∀ᶠ (x : α) in l, AEStronglyMeasurable (fun i => f (i, x)) (μ.restrict s)
hs : MeasurableSet s
hμ : μ s < ⊤
C : ℝ
hC :
  ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l,
    ‖f x‖ ≤
      C *
        ‖match x with
          | (_i, x) => g x‖
t : Set (ι × α)
htl : t ∈ 𝓟 s ×ˢ l
ht :
  ∀ y ∈ t,
    ‖f y‖ ≤
      C *
        ‖match y with
          | (_i, x) => g x‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
⊢ ∀ᶠ (x : α) in l, IntegrableOn (fun i => f (i, x)) s μ
Tactic:
obtain ⟨w, hwl, hw⟩ := hfm.exists_mem
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
f✝ : α → E
g : α → F
a b : α
μ✝ : Measure α
l : Filter α
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
ι : Type u_4
inst✝¹ : MeasurableSpace ι
f : ι × α → E
s : Set ι
μ : Measure ι
inst✝ : Norm F
hf :
  f =O[𝓟 s ×ˢ l] fun x =>
    match x with
    | (_i, x) => g x
hfm : ∀ᶠ (x : α) in l, AEStronglyMeasurable (fun i => f (i, x)) (μ.restrict s)
hs : MeasurableSet s
hμ : μ s < ⊤
C : ℝ
hC :
  ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l,
    ‖f x‖ ≤
      C *
        ‖match x with
          | (_i, x) => g x‖
t : Set (ι × α)
htl : t ∈ 𝓟 s ×ˢ l
ht :
  ∀ y ∈ t,
    ‖f y‖ ≤
      C *
        ‖match y with
          | (_i, x) => g x‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
w : Set α
hwl : w ∈ l
hw : ∀ y ∈ w, AEStronglyMeasurable (fun i => f (i, y)) (μ.restrict s)
⊢ ∀ᶠ (x : α) in l, IntegrableOn (fun i => f (i, x)) s μ