Theorem: MeasureTheory.LocallyIntegrable.integrable_of_isBigO_atTop_of_norm_eq_norm_neg (PrimeNumberTheoremAnd/Mathlib/MeasureTheory/Integral/Asymptotics.lean)

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 μ
⊢ Integrable f μ
Tactic:
refine (isEmpty_or_nonempty α).casesOn (fun _ ↦ Integrable.of_finite μ f) (fun _ ↦ ?_)
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 α
⊢ Integrable f μ

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 α
⊢ Integrable f μ
Tactic:
let a := -|Classical.arbitrary α|
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 α|
⊢ Integrable f μ

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 α|
⊢ Integrable f μ
Tactic:
have h_int : IntegrableOn f (Ici a) μ :=
  LocallyIntegrableOn.integrableOn_of_isBigO_atTop (hf.locallyIntegrableOn _) ho hg
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) μ
⊢ Integrable f μ

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) μ
⊢ Integrable f μ
Tactic:
have h_map_neg : (μ.restrict (Ici a)).map Neg.neg = μ.restrict (Iic (-a)) := by
  rw [show Ici a = Neg.neg ⁻¹' Iic (-a) by simp, ← measurableEmbedding_neg.restrict_map,
    Measure.map_neg_eq_self]
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))
⊢ Integrable f μ

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
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 μ

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
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 μ

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
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 μ

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 ?_
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 μ

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⟩
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

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
State after:
no goals

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]
State after:
no goals

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
State after:
no goals

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
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))

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
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)))

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
State after:
no goals

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]
State after:
no goals