Source indexedtheorem · leanprover/lean4:v4.32.0

MeasureTheory.eLpNorm_eq_eLpNorm_liftIoc

Carleson.ToMathlib.MeasureTheory.Integral.IntervalIntegral.Periodic · Carleson/ToMathlib/MeasureTheory/Integral/IntervalIntegral/Periodic.lean:130 to 136

Mathematical statement

Exact Lean statement

theorem MeasureTheory.eLpNorm_eq_eLpNorm_liftIoc {T : ℝ} [hT : Fact (0 < T)] {t : ℝ} {f : ℝ → ℂ}
  (hf : AEStronglyMeasurable f (volume.restrict (Ioc t (t + T)))) {p : ℝ≥0∞} :
    eLpNorm f p (volume.restrict (Ioc t (t + T))) = eLpNorm (AddCircle.liftIoc T t f) p volume

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem MeasureTheory.eLpNorm_eq_eLpNorm_liftIoc {T : ℝ} [hT : Fact (0 < T)] {t : ℝ} {f : ℝ → ℂ}  (hf : AEStronglyMeasurable f (volume.restrict (Ioc t (t + T)))) {p : ℝ≥0∞} :    eLpNorm f p (volume.restrict (Ioc t (t + T))) = eLpNorm (AddCircle.liftIoc T t f) p volume := by  simp only [AddCircle.liftIoc, Set.restrict_def, Function.comp_def]  rw [← Function.comp_def, eLpNorm_comp_measurePreserving (g := f) (p := p) hf]  refine .comp (measurePreserving_subtype_coe measurableSet_Ioc) ?_  exact AddCircle.measurePreserving_equivIoc T