Periodic.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 981 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Pinned Carleson blueprint

8 declarations, 0 contain sorry, 0 declared as axioms

Imports (1)

Carleson.ToMathlib.MeasureTheory.Integral.Periodic

Imported by 3 files

theorem Function.Periodic.setIntegral_Ioc_add_eq If f is a periodic function with period T, then its integral over [t, t + T] does not depend on t line 24 source
Source documentation
If f is a periodic function with period T, then its integral over [t, t + T] does not depend on t.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, NormedSpace, Real, Function.Periodic, Eq, MeasureTheory.integral, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, Set.Ioc, HAdd.hAdd
Proof uses: LT.lt, OfNat.ofNat, Not, Or, Classical.em, MeasureTheory.VAddInvariantMeasure, Subtype, Membership.mem, AddSubgroup, AddSubgroup.zmultiples, MeasureTheory.VAddInvariantMeasure.mk, Set, MeasurableSet, MeasureTheory.measure_preimage_add, MeasureTheory.IsAddFundamentalDomain.setIntegral_eq, isAddFundamentalDomain_Ioc, Function.Periodic.map_vadd_zmultiples, Eq.mpr, EmptyCollection.emptyCollection, id and 6 more
79 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
theorem setIntegral_Ioc_add_eq (hf : Periodic f T) (t s : ℝ) :
    ∫ x in Ioc t (t + T), f x = ∫ x in Ioc s (s + T), f x := by
…
```
Mentions: T, s
theorem Function.Periodic.setLIntegral_Ioc_add_eq line 33 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, ENNReal, Function.Periodic, Eq, MeasureTheory.lintegral, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, Set.Ioc, HAdd.hAdd
Proof uses: LT.lt, OfNat.ofNat, Not, Or, Classical.em, MeasureTheory.VAddInvariantMeasure, Subtype, Membership.mem, AddSubgroup, AddSubgroup.zmultiples, MeasureTheory.VAddInvariantMeasure.mk, Set, MeasurableSet, MeasureTheory.measure_preimage_add, MeasureTheory.IsAddFundamentalDomain.setLIntegral_eq, isAddFundamentalDomain_Ioc, Function.Periodic.map_vadd_zmultiples, Function.comp, ENorm.enorm, Function.Periodic.comp and 9 more
77 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
theorem Function.Periodic.eLpNorm TODO: the assumption p ≠ ⊤ is not necessary; this case should be proved as well line 44 source
Source comment
TODO: the assumption `p ≠ ⊤` is not necessary; this case should be proved as well

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Complex, Function.Periodic, ENNReal, Ne, Top.top, Eq, MeasureTheory.eLpNorm, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, Set.Ioc, HAdd.hAdd
Proof uses: id, dite, ite, OfNat.ofNat, MeasureTheory.eLpNormEssSup, MeasureTheory.eLpNorm', ENNReal.toReal, Eq.mpr, congr, congrArg, Eq.trans, ite_congr, Eq.refl, Not, ite_eq_right, ite_eq_left, HPow.hPow, MeasureTheory.lintegral, ENorm.enorm, HDiv.hDiv and 5 more
47 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
```
theorem eLpNorm {T : ℝ} {s t : ℝ} {f : ℝ → ℂ}
  (periodic_f : f.Periodic T)
  {p : ℝ≥0∞} (hp : p ≠ ⊤) :
    eLpNorm f p (volume.restrict (Ioc t (t + T))) = eLpNorm f p (volume.restrict (Ioc s (s + T))) := by
…
```
Mentions: T, s
theorem Function.Periodic.aestronglyMeasurable line 60 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Fact, LT.lt, OfNat.ofNat, Complex, Function.Periodic, MeasureTheory.AEStronglyMeasurable, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, Set.Ioc, HAdd.hAdd
Proof uses: Eq.mpr, Set.univ, id, Eq, congrArg, MeasureTheory.Measure, Eq.symm, MeasureTheory.Measure.restrict_univ, Set.iUnion, Int, HSMul.hSMul, Set, iUnion_Ioc_add_zsmul, Fact.out, MeasureTheory.AEStronglyMeasurable.iUnion, Function.comp, HSub.hSub, MeasureTheory.AEStronglyMeasurable.comp_measurePreserving, Set.preimage, Set.preimage_sub_const_Ioc and 55 more
136 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
theorem Function.Periodic.aestronglyMeasurable_iff line 79 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Fact, LT.lt, OfNat.ofNat, Complex, Function.Periodic, Iff, MeasureTheory.AEStronglyMeasurable, MeasureTheory.MeasureSpace.volume, MeasureTheory.Measure.restrict, Set.Ioc, HAdd.hAdd
Proof uses: Iff.intro, MeasureTheory.AEStronglyMeasurable.restrict, Function.Periodic.aestronglyMeasurable
32 instances, coercions and auxiliary constants left out.
lemma AddCircle.volume_preimage_equivIoc line 114 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Fact, LT.lt, OfNat.ofNat, Set, MeasurableSet, Eq, ENNReal, MeasureTheory.Measure, AddCircle, MeasureTheory.MeasureSpace.volume, Set.preimage, Membership.mem, Set.Ioc, HAdd.hAdd, Equiv, AddCircle.equivIoc, Inter.inter
Proof uses: Eq.mpr, MeasureTheory.Measure.restrict, id, congrArg, Eq.symm, MeasureTheory.Measure.restrict_apply', measurableSet_Ioc, AddSubgroup.zmultiples, MeasureTheory.MeasurePreserving.measure_preimage, AddCircle.measurePreserving_mk, Measurable.nullMeasurable, Measurable.subtype_coe, AddCircle.measurable_equivIoc, eq_of_heq, HEq, DFunLike, HEq.refl, Eq.refl, heq_of_eq, Set.ext and 11 more
80 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
theorem MeasureTheory.eLpNorm_eq_eLpNorm_liftIoc Analogous to MeasureTheory.MemLp.memLp_liftIoc line 130 source
Source comment
Analogous to `MeasureTheory.MemLp.memLp_liftIoc`

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Fact, LT.lt, OfNat.ofNat, Complex, MeasureTheory.AEStronglyMeasurable, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, Set.Ioc, HAdd.hAdd, ENNReal, Eq, MeasureTheory.eLpNorm, AddCircle, AddCircle.liftIoc
Proof uses: id, Eq.mpr, Membership.mem, Set, Equiv, AddCircle.equivIoc, Function.comp, congrArg, Eq.symm, Function.comp_def, MeasureTheory.eLpNorm_comp_measurePreserving, MeasureTheory.MeasurePreserving.comp, MeasureTheory.Measure.comap, Subtype, MeasureTheory.measurePreserving_subtype_coe, measurableSet_Ioc, AddCircle.measurePreserving_equivIoc, Eq.refl
80 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
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
…
```
Mentions: T
theorem MeasureTheory.eLpNorm_eq_eLpNorm_liftIoc' TODO: find better name line 139 source
Source comment
TODO: find better name

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Fact, LT.lt, OfNat.ofNat, AddCircle, Complex, MeasureTheory.AEStronglyMeasurable, AddSubgroup.zmultiples, MeasureTheory.MeasureSpace.volume, ENNReal, Eq, MeasureTheory.eLpNorm, MeasureTheory.Measure.restrict, Set.Ioc, HAdd.hAdd
Proof uses: Eq.mpr, AddCircle.liftIoc, id, congrArg, MeasureTheory.eLpNorm_eq_eLpNorm_liftIoc, MeasureTheory.AEStronglyMeasurable.comp_measurePreserving, AddCircle.measurePreserving_mk, ENorm, MeasurableSpace, Eq.rec, MeasureTheory.Measure, Eq.refl, funext, of_eq_true, Function.comp, Set.domRestrict, Equiv, AddCircle.equivIoc, Eq.trans, True and 7 more
75 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
theorem MeasureTheory.eLpNorm_eq_eLpNorm_liftIoc' {T : ℝ} [hT : Fact (0 < T)] {t : ℝ}
  {f : (AddCircle T) → ℂ} (hf : AEStronglyMeasurable f volume) {p : ℝ≥0∞} :
    eLpNorm (fun (x : ℝ) ↦ f x) p (volume.restrict (Ioc t (t + T))) = eLpNorm f p volume := by
…
```
Mentions: T