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

23 declarations, 0 contain sorry, 0 declared as axioms

Imports (3)

Imported by 3 files

instance AddCircle.noAtoms_volume line 23 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Fact, LT.lt, OfNat.ofNat, MeasureTheory.NullSingletonClass, AddCircle, MeasureTheory.MeasureSpace.volume
Proof uses: MeasureTheory.NullSingletonClass.mk, Eq.mpr, Eq, ENNReal, MeasureTheory.Measure, Set, Singleton.singleton, AddSubgroup.zmultiples, id, congrFun', congrArg, MeasureTheory.Measure.addHaar_singleton, Eq.mp, Metric.closedBall, ENNReal.ofReal, Min.min, HMul.hMul, Nat, congr, Eq.trans and 7 more
74 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem AddCircle.liftIoc_ae_eq_liftIco line 28 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Fact, LT.lt, OfNat.ofNat, Filter.EventuallyEq, AddCircle, MeasureTheory.ae, MeasureTheory.Measure, MeasureTheory.MeasureSpace.volume, AddCircle.liftIoc, AddCircle.liftIco
Proof uses: Filter.Eventually.mono, Ne, AddSubgroup.zmultiples, Eq, MeasureTheory.Measure.ae_ne, AddCircle.liftIoc_eq_liftIco_of_ne
25 instances, coercions and auxiliary constants left out.
theorem AddCircle.measurable_equivIoc Add before measurableEquivIoc line 38 source
Source comment
Add before `measurableEquivIoc`

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Fact, LT.lt, OfNat.ofNat, Measurable, AddCircle, Set.Ioc, HAdd.hAdd, AddSubgroup.zmultiples, Membership.mem, Set, Equiv, AddCircle.equivIoc
Proof uses: measurable_of_measurable_on_compl_singleton, Continuous.measurable, Eq, False, Set.domRestrict, Iff.mp, ContinuousOn, Continuous, continuousOn_iff_continuous_domRestrict, continuousOn_of_forall_continuousAt, AddCircle.continuousAt_equivIoc
117 instances, coercions and auxiliary constants left out.
```
theorem measurable_equivIoc (a : ℝ) : Measurable (equivIoc T a) :=
…
```
Mentions: T
theorem AddCircle.measurable_equivIco line 43 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Fact, LT.lt, OfNat.ofNat, Measurable, AddCircle, Set.Ico, HAdd.hAdd, AddSubgroup.zmultiples, Membership.mem, Set, Equiv, AddCircle.equivIco
Proof uses: measurable_of_measurable_on_compl_singleton, Continuous.measurable, Eq, False, Set.domRestrict, Iff.mp, ContinuousOn, Continuous, continuousOn_iff_continuous_domRestrict, continuousOn_of_forall_continuousAt, AddCircle.continuousAt_equivIco
117 instances, coercions and auxiliary constants left out.
def AddCircle.measurableEquivIoc' Replacement for existing proof of measurableEquivIoc now that the proof of measurable_toFun is extracted as a separate lemma line 50 source
Source comment
Replacement for existing proof of `measurableEquivIoc` now that the proof of `measurable_toFun` is extracted as a separate lemma. The name is primed here only to avoid a collision.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Fact, LT.lt, OfNat.ofNat, MeasurableEquiv, AddCircle, Set.Ioc, HAdd.hAdd, AddSubgroup.zmultiples, Membership.mem, Set
Proof uses: Equiv, AddCircle.equivIoc, MeasurableEquiv.mk, AddCircle.measurable_equivIoc
30 instances, coercions and auxiliary constants left out.
```
noncomputable def measurableEquivIoc' (a : ℝ) : AddCircle T ≃ᵐ Ioc a (a + T) where
…
```
Mentions: T
def AddCircle.measurableEquivIco' Replacement for existing proof of measurableEquivIco now that the proof of measurable_toFun is extracted as a separate lemma line 57 source
Source comment
Replacement for existing proof of `measurableEquivIco` now that the proof of `measurable_toFun` is extracted as a separate lemma. The name is primed here only to avoid a collision.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Fact, LT.lt, OfNat.ofNat, MeasurableEquiv, AddCircle, Set.Ico, HAdd.hAdd, AddSubgroup.zmultiples, Membership.mem, Set
Proof uses: Equiv, AddCircle.equivIco, MeasurableEquiv.mk, AddCircle.measurable_equivIco
30 instances, coercions and auxiliary constants left out.
```
noncomputable def measurableEquivIco' (a : ℝ) : AddCircle T ≃ᵐ Ico a (a + T) where
…
```
Mentions: T
lemma AddCircle.map_subtypeVal_map_equivIoc_volume line 64 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Fact, LT.lt, OfNat.ofNat, Eq, MeasureTheory.Measure, MeasureTheory.Measure.map, Subtype, Membership.mem, Set, Set.Ioc, HAdd.hAdd, AddCircle, Equiv, AddCircle.equivIoc, MeasureTheory.MeasureSpace.volume, MeasureTheory.Measure.restrict
Proof uses: Measurable, AddSubgroup.zmultiples, AddCircle.measurable_equivIoc, Eq.mpr, id, congrArg, Eq.symm, MeasureTheory.MeasurePreserving.map_eq, AddCircle.measurePreserving_mk, Function.comp, MeasureTheory.Measure.map_map, measurable_subtype_coe, Measurable.comp, MeasurableSet, Eq.trans, AddCircle.liftIoc, Set.ofPred, And, LE.le, MeasureTheory.Measure.map_congr and 6 more
77 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
theorem MeasureTheory.AEStronglyMeasurable.liftIoc line 82 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Fact, LT.lt, OfNat.ofNat, TopologicalSpace, MeasureTheory.AEStronglyMeasurable, MeasureTheory.MeasureSpace.volume, AddCircle, AddSubgroup.zmultiples, AddCircle.liftIoc
Proof uses: MeasureTheory.AEStronglyMeasurable.comp_measurable, Subtype, Membership.mem, Set, Set.Ioc, HAdd.hAdd, Function.comp, Equiv, AddCircle.equivIoc, MeasureTheory.Measure.map, Eq.rec, MeasureTheory.Measure, MeasureTheory.Measure.restrict, Eq, MeasureTheory.AEStronglyMeasurable.restrict, Eq.symm, AddCircle.map_subtypeVal_map_equivIoc_volume, measurable_subtype_coe, AddCircle.measurable_equivIoc
43 instances, coercions and auxiliary constants left out.
theorem MeasureTheory.AEStronglyMeasurable.liftIco line 87 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Fact, LT.lt, OfNat.ofNat, TopologicalSpace, MeasureTheory.AEStronglyMeasurable, MeasureTheory.MeasureSpace.volume, AddCircle, AddSubgroup.zmultiples, AddCircle.liftIco
Proof uses: MeasureTheory.AEStronglyMeasurable.congr, AddCircle.liftIoc, MeasureTheory.AEStronglyMeasurable.liftIoc, AddCircle.liftIoc_ae_eq_liftIco
26 instances, coercions and auxiliary constants left out.
theorem MeasureTheory.AEMeasurable.liftIoc line 91 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Fact, LT.lt, OfNat.ofNat, MeasurableSpace, AEMeasurable, MeasureTheory.MeasureSpace.volume, AddCircle, AddCircle.liftIoc
Proof uses: AEMeasurable.comp_measurable, Subtype, Membership.mem, Set, Set.Ioc, HAdd.hAdd, Equiv, AddCircle.equivIoc, Function.comp, MeasureTheory.Measure.map, Eq.rec, MeasureTheory.Measure, MeasureTheory.Measure.restrict, Eq, AEMeasurable.restrict, Eq.symm, AddCircle.map_subtypeVal_map_equivIoc_volume, measurable_subtype_coe, AddCircle.measurable_equivIoc
40 instances, coercions and auxiliary constants left out.
theorem MeasureTheory.AEMeasurable.liftIco line 96 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Fact, LT.lt, OfNat.ofNat, MeasurableSpace, AEMeasurable, MeasureTheory.MeasureSpace.volume, AddCircle, AddCircle.liftIco
Proof uses: AEMeasurable.congr, AddCircle.liftIoc, MeasureTheory.AEMeasurable.liftIoc, AddCircle.liftIoc_ae_eq_liftIco
20 instances, coercions and auxiliary constants left out.
theorem MeasureTheory.map_coe_addCircle_volume_eq line 100 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Fact, LT.lt, OfNat.ofNat, Eq, MeasureTheory.Measure, HasQuotient.Quotient, AddSubgroup, AddSubgroup.zmultiples, MeasureTheory.Measure.map, MeasureTheory.MeasureSpace.volume, HSMul.hSMul, ENNReal, AddCircle, Top.top
Proof uses: MeasureTheory.Measure.sum, Int, MeasureTheory.Measure.restrict, Set.Ioc, HAdd.hAdd, Eq.mpr, Set.iUnion, id, congrArg, Eq.symm, MeasureTheory.Measure.restrict_iUnion, Set.pairwise_disjoint_Ioc_zsmul, measurableSet_Ioc, Set.univ, Set, iUnion_Ioc_zsmul, Fact.out, MeasureTheory.Measure.restrict_univ, Eq.refl, MeasureTheory.Measure.map_sum and 28 more
106 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
theorem MeasureTheory.quasiMeasurePreserving_coe_addCircle line 116 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Fact, LT.lt, OfNat.ofNat, MeasureTheory.Measure.QuasiMeasurePreserving, HasQuotient.Quotient, AddSubgroup, AddSubgroup.zmultiples, MeasureTheory.MeasureSpace.volume
Proof uses: MeasureTheory.Measure.QuasiMeasurePreserving.mk, AddCircle.measurable_mk', Eq.mpr, MeasureTheory.Measure.AbsolutelyContinuous, MeasureTheory.Measure.map, HSMul.hSMul, ENNReal, MeasureTheory.Measure, AddCircle, Top.top, id, Eq, congrArg, MeasureTheory.map_coe_addCircle_volume_eq, MeasureTheory.Measure.smul_absolutelyContinuous
32 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
theorem AddCircle.liftIco_convolution_liftIco line 135 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, NontriviallyNormedField, NormedSpace, Real, ContinuousLinearMap, RingHom.id, Fact, LT.lt, OfNat.ofNat, Function.Periodic, Eq, AddCircle, MeasureTheory.convolution, AddSubgroup.zmultiples, AddCircle.liftIco, MeasureTheory.MeasureSpace.volume, intervalIntegral, HSub.hSub, HAdd.hAdd
Proof uses: funext, QuotientAddGroup.induction_on, intervalIntegral.integral_congr, Membership.mem, Set, Set.uIcc, Eq.mpr, id, congrArg, add_sub_right_comm, Eq.refl, MeasureTheory.integral, MeasureTheory.convolution.eq_1, Eq.symm, AddCircle.intervalIntegral_preimage, AddCircle.liftIco_coe_apply_of_periodic
152 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
theorem AddCircle.liftIoc_convolution_liftIoc line 145 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, NontriviallyNormedField, NormedSpace, Real, ContinuousLinearMap, RingHom.id, Fact, LT.lt, OfNat.ofNat, Function.Periodic, Eq, AddCircle, MeasureTheory.convolution, AddSubgroup.zmultiples, AddCircle.liftIoc, MeasureTheory.MeasureSpace.volume, intervalIntegral, HSub.hSub, HAdd.hAdd
Proof uses: intervalIntegral.integral_congr, Membership.mem, Set, Set.uIcc, Eq.mpr, id, congrArg, add_sub_right_comm, Eq.refl, AddCircle.liftIco, Eq.symm, AddCircle.liftIco_eq_liftIoc, AddCircle.liftIco_convolution_liftIco
147 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
theorem AddCircle.eLpNorm_liftIoc The norm of the lift of a function f is equal to the norm of f on that period line 162 source
Source documentation
The norm of the lift of a function f is equal to the norm of f on that period.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, Real, Fact, LT.lt, OfNat.ofNat, MeasureTheory.AEStronglyMeasurable, MeasureTheory.MeasureSpace.volume, ENNReal, Eq, MeasureTheory.eLpNorm, AddCircle, AddCircle.liftIoc, Set.indicator, Set.Ioc, HAdd.hAdd
Proof uses: Set, Eq.mpr, id, congrArg, rfl, Function.comp, AddSubgroup.zmultiples, funext, dite, Membership.mem, congr, Set.indicator_of_mem, Eq.symm, AddCircle.liftIoc_coe_apply, Not, of_eq_true, Eq.trans, True, Set.indicator_of_notMem, False and 9 more
84 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
theorem eLpNorm_liftIoc (p : ℝ≥0∞) :
    eLpNorm (AddCircle.liftIoc T a f) p = eLpNorm ((Set.Ioc a (a + T)).indicator f) p := by
…
```
Mentions: T
theorem AddCircle.eLpNorm_liftIoc' The norm of the lift of a function f is equal to the norm of f on that period line 174 source
Source documentation
The norm of the lift of a function f is equal to the norm of f on that period.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, Real, Fact, LT.lt, OfNat.ofNat, MeasureTheory.AEStronglyMeasurable, MeasureTheory.MeasureSpace.volume, ENNReal, Eq, MeasureTheory.eLpNorm, AddCircle, AddCircle.liftIoc, MeasureTheory.Measure.restrict, Set.Ioc, HAdd.hAdd
Proof uses: Eq.mpr, Set.indicator, id, congrArg, AddCircle.eLpNorm_liftIoc, MeasureTheory.eLpNorm_indicator_eq_eLpNorm_restrict, measurableSet_Ioc, Eq.refl
71 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem eLpNorm_liftIoc' (p : ℝ≥0∞) :
    eLpNorm (AddCircle.liftIoc T a f) p = eLpNorm f p (volume.restrict ((Set.Ioc a (a + T)))) := by
…
```
Mentions: T
theorem AddCircle.eLpNorm_liftIco The norm of the lift of a function f is equal to the norm of f on that period line 179 source
Source documentation
The norm of the lift of a function f is equal to the norm of f on that period.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, Real, Fact, LT.lt, OfNat.ofNat, MeasureTheory.AEStronglyMeasurable, MeasureTheory.MeasureSpace.volume, ENNReal, Eq, MeasureTheory.eLpNorm, AddCircle, AddCircle.liftIco, Set.indicator, Set.Ico, HAdd.hAdd
Proof uses: Eq.mpr, AddCircle.liftIoc, id, congrArg, MeasureTheory.eLpNorm_congr_ae, Filter.EventuallyEq.symm, MeasureTheory.ae, MeasureTheory.Measure, AddCircle.liftIoc_ae_eq_liftIco, Set.Ioc, AddCircle.eLpNorm_liftIoc, MeasureTheory.Measure.restrict, MeasureTheory.eLpNorm_indicator_eq_eLpNorm_restrict, measurableSet_Ico, measurableSet_Ioc, MeasureTheory.restrict_Ico_eq_restrict_Ioc, Eq.refl
82 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem eLpNorm_liftIco (p : ℝ≥0∞) :
    eLpNorm (AddCircle.liftIco T a f) p = eLpNorm ((Set.Ico a (a + T)).indicator f) p := by
…
```
Mentions: T
theorem AddCircle.eLpNorm_liftIco' The norm of the lift of a function f is equal to the norm of f on that period line 186 source
Source documentation
The norm of the lift of a function f is equal to the norm of f on that period.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, Real, Fact, LT.lt, OfNat.ofNat, MeasureTheory.AEStronglyMeasurable, MeasureTheory.MeasureSpace.volume, ENNReal, Eq, MeasureTheory.eLpNorm, AddCircle, AddCircle.liftIco, MeasureTheory.Measure.restrict, Set.Ico, HAdd.hAdd
Proof uses: Eq.mpr, Set.indicator, id, congrArg, AddCircle.eLpNorm_liftIco, MeasureTheory.eLpNorm_indicator_eq_eLpNorm_restrict, measurableSet_Ico, Eq.refl
71 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem eLpNorm_liftIco' (p : ℝ≥0∞) :
    eLpNorm (AddCircle.liftIco T a f) p = eLpNorm f p (volume.restrict (Set.Ico a (a + T))) := by
…
```
Mentions: T
theorem AddCircle.eLpNorm_liftIoc_of_periodic The norm of the lift of a periodic function f is equal to the norm of f on any period line 191 source
Source documentation
The norm of the lift of a periodic function f is equal to the norm of f on any period.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, Real, Fact, LT.lt, OfNat.ofNat, MeasureTheory.AEStronglyMeasurable, MeasureTheory.MeasureSpace.volume, Function.Periodic, ENNReal, Eq, MeasureTheory.eLpNorm, AddCircle, AddCircle.liftIoc, Set.indicator, Set.Ioc, HAdd.hAdd
Proof uses: Eq.mpr, id, congrArg, AddCircle.liftIoc_eq_liftIoc, AddCircle.eLpNorm_liftIoc, Eq.refl
56 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem eLpNorm_liftIoc_of_periodic (hfT : Periodic f T) (p : ℝ≥0∞) :
    eLpNorm (AddCircle.liftIoc T a f) p = eLpNorm ((Set.Ioc a' (a' + T)).indicator f) p := by
…
```
Mentions: T
theorem AddCircle.eLpNorm_liftIoc_of_periodic' The norm of the lift of a periodic function f is equal to the norm of f on any period line 196 source
Source documentation
The norm of the lift of a periodic function f is equal to the norm of f on any period.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, Real, Fact, LT.lt, OfNat.ofNat, MeasureTheory.AEStronglyMeasurable, MeasureTheory.MeasureSpace.volume, Function.Periodic, ENNReal, Eq, MeasureTheory.eLpNorm, AddCircle, AddCircle.liftIoc, MeasureTheory.Measure.restrict, Set.Ioc, HAdd.hAdd
Proof uses: Eq.mpr, Set.indicator, id, congrArg, AddCircle.eLpNorm_liftIoc_of_periodic, MeasureTheory.eLpNorm_indicator_eq_eLpNorm_restrict, measurableSet_Ioc, Eq.refl
71 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem eLpNorm_liftIoc_of_periodic' (hfT : Periodic f T) (p : ℝ≥0∞) :
    eLpNorm (AddCircle.liftIoc T a f) p = eLpNorm f p (volume.restrict (Set.Ioc a' (a' + T))) := by
…
```
Mentions: T
theorem AddCircle.eLpNorm_liftIco_of_periodic The norm of the lift of a periodic function f is equal to the norm of f on any period line 202 source
Source documentation
The norm of the lift of a periodic function f is equal to the norm of f on any period.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, Real, Fact, LT.lt, OfNat.ofNat, MeasureTheory.AEStronglyMeasurable, MeasureTheory.MeasureSpace.volume, Function.Periodic, ENNReal, Eq, MeasureTheory.eLpNorm, AddCircle, AddCircle.liftIco, Set.indicator, Set.Ico, HAdd.hAdd
Proof uses: Eq.mpr, id, congrArg, AddCircle.liftIco_eq_liftIco, AddCircle.eLpNorm_liftIco, Eq.refl
56 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem eLpNorm_liftIco_of_periodic (hfT : Periodic f T) (p : ℝ≥0∞) :
    eLpNorm (AddCircle.liftIco T a f) p = eLpNorm ((Set.Ico a' (a' + T)).indicator f) p := by
…
```
Mentions: T
theorem AddCircle.eLpNorm_liftIco_of_periodic' The norm of the lift of a periodic function f is equal to the norm of f on any period line 207 source
Source documentation
The norm of the lift of a periodic function f is equal to the norm of f on any period.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, Real, Fact, LT.lt, OfNat.ofNat, MeasureTheory.AEStronglyMeasurable, MeasureTheory.MeasureSpace.volume, Function.Periodic, ENNReal, Eq, MeasureTheory.eLpNorm, AddCircle, AddCircle.liftIco, MeasureTheory.Measure.restrict, Set.Ico, HAdd.hAdd
Proof uses: Eq.mpr, Set.indicator, id, congrArg, AddCircle.eLpNorm_liftIco_of_periodic, MeasureTheory.eLpNorm_indicator_eq_eLpNorm_restrict, measurableSet_Ico, Eq.refl
71 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem eLpNorm_liftIco_of_periodic' (hfT : Periodic f T) (p : ℝ≥0∞) :
    eLpNorm (AddCircle.liftIco T a f) p = eLpNorm f p (volume.restrict (Set.Ico a' (a' + T))) := by
…
```
Mentions: T