convert hf.aestronglyMeasurable.restrict
α : 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)))
no goals