Source indexedtheorem · leanprover/lean4:v4.32.0

AddCircle.eLpNorm_liftIoc

Carleson.ToMathlib.MeasureTheory.Integral.Periodic · Carleson/ToMathlib/MeasureTheory/Integral/Periodic.lean:163 to 172

Source documentation

The norm of the lift of a function f is equal to the norm of f on that period.

Exact Lean statement

theorem eLpNorm_liftIoc (p : ℝ≥0∞) :
    eLpNorm (AddCircle.liftIoc T a f) p = eLpNorm ((Set.Ioc a (a + T)).indicator f) p

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem eLpNorm_liftIoc (p : ℝ≥0∞) :    eLpNorm (AddCircle.liftIoc T a f) p = eLpNorm ((Set.Ioc a (a + T)).indicator f) p := by  set I := Ioc a (a + T)  have : I.indicator f = I.indicator (liftIoc T a f ∘ QuotientAddGroup.mk) := by    ext x    by_cases hx : x ∈ I    · simpa [hx] using (liftIoc_coe_apply hx).symm    · simp [hx]  rw [this, eLpNorm_indicator_eq_eLpNorm_restrict measurableSet_Ioc]  exact (eLpNorm_comp_measurePreserving (hf.liftIoc T a) (AddCircle.measurePreserving_mk T a)).symm