Basic.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

27 declarations, 0 contain sorry, 0 declared as axioms

Imports (5)

Imported by 5 files

theorem fourierCoeff_eq_fourierCoeff_of_aeeq TODO: I think the measurability assumptions might be unnecessary line 17 source
Source comment
TODO: I think the measurability assumptions might be unnecessary

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Fact, LT.lt, OfNat.ofNat, Int, AddCircle, Complex, MeasureTheory.AEStronglyMeasurable, AddSubgroup.zmultiples, AddCircle.haarAddCircle, Filter.EventuallyEq, MeasureTheory.ae, MeasureTheory.Measure, Eq, fourierCoeff
Proof uses: id, MeasureTheory.integral_congr_ae, HSMul.hSMul, ContinuousMap, fourier, Neg.neg, Measurable.aestronglyMeasurable, ContinuousMap.measurable, Eq.mpr, HMul.hMul, MeasureTheory.AEEqFun, MeasureTheory.AEEqFun.mk, MeasureTheory.AEStronglyMeasurable.mul, congrArg, Eq.symm, propext, MeasureTheory.AEEqFun.mk_eq_mk, MeasureTheory.AEEqFun.mk_mul_mk, HMul, Eq.rec and 1 more
107 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
theorem fourierCoeff_eq_fourierCoeff_of_aeeq {T : ℝ} [hT : Fact (0 < T)] {n : ℤ} {f g : AddCircle T → ℂ}
    (hf : AEStronglyMeasurable f haarAddCircle) (hg : AEStronglyMeasurable g haarAddCircle)
    (h : f =ᵐ[haarAddCircle] g) : fourierCoeff f n = fourierCoeff g n := by
…
```
Mentions: T, g
def partialFourierSum' line 29 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Fact, LT.lt, OfNat.ofNat, Nat, AddCircle, Complex, ContinuousMap, AddSubgroup.zmultiples
Proof uses: Finset.sum, Int, Finset.Icc, Neg.neg, Int.ofNat, HSMul.hSMul, fourierCoeff, fourier
51 instances, coercions and auxiliary constants left out.
theorem partialFourierSum'_comp_equivAddCircle line 32 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Fact, LT.lt, OfNat.ofNat, AddCircle, Complex, Nat, Eq, ContinuousMap, AddSubgroup.zmultiples, partialFourierSum', AddEquiv, AddCircle.equivAddCircle, LT.lt.ne', Fact.out
Proof uses: id, Eq.mpr, Finset.sum, Int, Finset.Icc, Neg.neg, Int.ofNat, HSMul.hSMul, fourierCoeff, fourier, HMul.hMul, congr, congrArg, Eq.trans, congrFun, ContinuousMap.coe_sum, Finset.sum_congr, Eq.refl, Finset, Membership.mem and 7 more
84 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
def partialFourierSumLp line 45 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Fact, LT.lt, OfNat.ofNat, ENNReal, LE.le, Nat, AddCircle, Complex, Subtype, MeasureTheory.AEEqFun, AddSubgroup.zmultiples, AddCircle.haarAddCircle, Membership.mem, AddSubgroup, MeasureTheory.Lp
Proof uses: Finset.sum, Int, Finset.Icc, Neg.neg, Int.ofNat, HSMul.hSMul, fourierCoeff, fourierLp
76 instances, coercions and auxiliary constants left out.
lemma partialFourierSum_eq_partialFourierSum' line 53 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Eq, AddCircle, HMul.hMul, OfNat.ofNat, Real.pi, AddCircle.liftIoc, instFactLtRealOfNatHMulPi, partialFourierSum, ContinuousMap, AddSubgroup.zmultiples, partialFourierSum'
Proof uses: funext, id, Finset.sum, Int, Finset.Icc, Neg.neg, fourierCoeffOn, Real.two_pi_pos, fourier, Int.ofNat, HSMul.hSMul, fourierCoeff, Eq.mpr, Function.comp, Set.Ioc, HAdd.hAdd, Set.domRestrict, Equiv, AddCircle.equivIoc, Membership.mem and 38 more
117 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
lemma partialFourierSum_eq_partialFourierSum'_apply line 73 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, AddCircle, HMul.hMul, OfNat.ofNat, Real.pi, Eq, AddCircle.liftIoc, instFactLtRealOfNatHMulPi, partialFourierSum, ContinuousMap, AddSubgroup.zmultiples, partialFourierSum'
Proof uses: Eq.mpr, id, congrArg, partialFourierSum_eq_partialFourierSum', Eq.refl
50 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma partialFourierSum'_eq_partialFourierSum_apply line 79 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, AddCircle, Real, HMul.hMul, OfNat.ofNat, Real.pi, Complex, Membership.mem, Set, Set.Ioc, Eq, ContinuousMap, AddSubgroup.zmultiples, partialFourierSum', instFactLtRealOfNatHMulPi, partialFourierSum
Proof uses: AddCircle.liftIoc, id, AddCommMonoid, Finset, Eq.rec, Finset.sum, Eq.refl, Int, Finset.Icc, Neg.neg, Int.ofNat, HSMul.hSMul, fourierCoeff, fourier, funext, ContinuousMap.ext, DFunLike, HSMul, Eq.mpr, congrArg and 29 more
99 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
lemma partialFourierSupLp_eq_partialFourierSupLp_of_aeeq line 94 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Fact, LT.lt, OfNat.ofNat, ENNReal, LE.le, Nat, AddCircle, Complex, MeasureTheory.AEStronglyMeasurable, AddSubgroup.zmultiples, AddCircle.haarAddCircle, Filter.EventuallyEq, MeasureTheory.ae, MeasureTheory.Measure, Eq, Subtype, MeasureTheory.AEEqFun, Membership.mem, AddSubgroup and 2 more
Proof uses: id, AddCommMonoid, Finset, Eq.rec, Finset.sum, Eq.refl, Int, Finset.Icc, Neg.neg, Int.ofNat, HSMul.hSMul, fourierCoeff, fourierLp, funext, HSMul, fourierCoeff_eq_fourierCoeff_of_aeeq
89 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma partialFourierSum'_eq_partialFourierSumLp line 104 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Fact, LT.lt, OfNat.ofNat, ENNReal, LE.le, Nat, AddCircle, Complex, Eq, Subtype, MeasureTheory.AEEqFun, AddSubgroup.zmultiples, AddCircle.haarAddCircle, Membership.mem, AddSubgroup, MeasureTheory.Lp, partialFourierSumLp, MeasureTheory.MemLp.toLp, ContinuousMap and 2 more
Proof uses: id, Finset.sum, Int, Finset.Icc, Neg.neg, Int.ofNat, HSMul.hSMul, fourierCoeff, fourierLp, fourier, Eq.mpr, ContinuousLinearMap, RingHom.id, ContinuousMap.toLp, MeasureTheory.MemLp, ContinuousMap.coe_sum, congrArg, MeasureTheory.MemLp.toLp.congr_simp, Finset.sum_congr, Eq.refl and 9 more
197 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma partialFourierSum_aeeq_partialFourierSumLp line 114 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Fact, LE.le, OfNat.ofNat, Nat, Real, Complex, MeasureTheory.MemLp, AddCircle, HMul.hMul, Real.pi, AddSubgroup.zmultiples, AddCircle.liftIoc, instFactLtRealOfNatHMulPi, AddCircle.haarAddCircle, Filter.EventuallyEq, MeasureTheory.ae, MeasureTheory.Measure, partialFourierSum, MeasureTheory.AEEqFun and 5 more
Proof uses: Eq.mpr, id, Eq, congrArg, Subtype, partialFourierSupLp_eq_partialFourierSupLp_of_aeeq, MeasureTheory.Lp.aestronglyMeasurable, MeasureTheory.MemLp.aestronglyMeasurable, MeasureTheory.MemLp.coeFn_toLp, ContinuousMap, partialFourierSum', ContinuousMap.memLp, partialFourierSum'_eq_partialFourierSumLp, partialFourierSum_eq_partialFourierSum', Filter.EventuallyEq.symm
135 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma fourierCoeffOn_mul line 127 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LT.lt, Complex, Int, Eq, fourierCoeffOn, HMul.hMul
Proof uses: fourierCoeffOn.const_mul
9 instances, coercions and auxiliary constants left out.
lemma fourierCoeffOn_neg line 132 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LT.lt, Complex, Int, Eq, fourierCoeffOn, Neg.neg
Proof uses: of_eq_true, Eq.trans, HMul.hMul, Inv.inv, HSub.hSub, intervalIntegral, RingHom, starRingEnd, Complex.exp, HDiv.hDiv, OfNat.ofNat, Nat, Real.pi, Complex.I, MeasureTheory.MeasureSpace.volume, True, congr, congrArg, HSMul.hSMul, ContinuousMap and 24 more
125 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma fourierCoeffOn_add line 137 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LT.lt, Complex, Int, IntervalIntegrable, MeasureTheory.MeasureSpace.volume, Eq, fourierCoeffOn, HAdd.hAdd
Proof uses: Eq.mpr, HSMul.hSMul, Inv.inv, HSub.hSub, intervalIntegral, HMul.hMul, RingHom, starRingEnd, Complex.exp, HDiv.hDiv, OfNat.ofNat, Nat, Real.pi, Complex.I, id, congr, congrArg, Eq.trans, ContinuousMap, AddCircle and 78 more
177 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma fourierCoeffOn_sub line 149 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LT.lt, Complex, Int, IntervalIntegrable, MeasureTheory.MeasureSpace.volume, Eq, fourierCoeffOn, HSub.hSub
Proof uses: Eq.mpr, HAdd.hAdd, Neg.neg, id, congrArg, sub_eq_add_neg, fourierCoeffOn_add, IntervalIntegrable.neg, fourierCoeffOn_neg, Eq.symm, Eq.refl
59 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma partialFourierSum_add line 156 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Complex, Nat, IntervalIntegrable, MeasureTheory.MeasureSpace.volume, OfNat.ofNat, HMul.hMul, Real.pi, Eq, partialFourierSum, HAdd.hAdd
Proof uses: funext, of_eq_true, Eq.trans, Finset.sum, Int, Finset.Icc, Neg.neg, fourierCoeffOn, Real.two_pi_pos, Complex.exp, HDiv.hDiv, Complex.I, True, congr, congrArg, ContinuousMap, AddCircle, AddSubgroup.zmultiples, fourier, Finset.sum_congr and 16 more
105 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma partialFourierSum_sub line 165 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Complex, Nat, IntervalIntegrable, MeasureTheory.MeasureSpace.volume, OfNat.ofNat, HMul.hMul, Real.pi, Eq, partialFourierSum, HSub.hSub
Proof uses: funext, of_eq_true, Eq.trans, Finset.sum, Int, Finset.Icc, Neg.neg, fourierCoeffOn, Real.two_pi_pos, Complex.exp, HDiv.hDiv, Complex.I, True, congr, congrArg, ContinuousMap, AddCircle, AddSubgroup.zmultiples, fourier, Finset.sum_congr and 16 more
111 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma partialFourierSum_mul line 174 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Complex, Nat, Eq, partialFourierSum, HMul.hMul
Proof uses: funext, of_eq_true, Eq.trans, Finset.sum, Int, Finset.Icc, Neg.neg, fourierCoeffOn, OfNat.ofNat, Real.pi, Real.two_pi_pos, Complex.exp, HDiv.hDiv, Complex.I, True, congr, congrArg, Finset.sum_congr, ContinuousMap, AddCircle and 18 more
82 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma fourier_periodic line 180 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, Function.Periodic, Real, Complex, ContinuousMap, AddCircle, HMul.hMul, OfNat.ofNat, Nat, Real.pi, AddSubgroup.zmultiples, fourier
Proof uses: of_eq_true, Eq, HAdd.hAdd, Eq.trans, True, forall_congr, Complex.exp, HDiv.hDiv, Complex.I, congr, congrArg, HasQuotient.Quotient, AddSubgroup, QuotientAddGroup.mk_add_of_mem, Membership.mem, Submonoid, Submonoid.unitSphere, AddCircle.toCircle, HSMul.hSMul, fourier_coe_apply' and 3 more
74 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma partialFourierSum_periodic line 184 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Complex, Nat, Function.Periodic, partialFourierSum, HMul.hMul, OfNat.ofNat, Real.pi
Proof uses: of_eq_true, Eq, HAdd.hAdd, Eq.trans, True, forall_congr, Finset.sum, Int, Finset.Icc, Neg.neg, fourierCoeffOn, Real.two_pi_pos, Complex.exp, HDiv.hDiv, Complex.I, congr, congrArg, Finset.sum_congr, ContinuousMap, AddCircle and 16 more
80 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Function.Periodic.uniformContinuous_of_continuous TODO: maybe generalize to (hc : ContinuousOn f (Set.Icc 0 T)) and leave out condition (hT : 0 < T) line 188 source
Source comment
TODO: maybe generalize to (hc : ContinuousOn f (Set.Icc 0 T)) and leave out condition (hT : 0 < T)

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Complex, LT.lt, OfNat.ofNat, Function.Periodic, ContinuousOn, Set.Icc, Neg.neg, HMul.hMul, Nat, UniformContinuous
Proof uses: IsCompact, CompactIccSpace.isCompact_Icc, UniformContinuousOn, IsCompact.uniformContinuousOn_of_continuous, Eq.mpr, GT.gt, Exists, And, Dist.dist, id, Eq, congrArg, propext, Metric.uniformContinuous_iff, Membership.mem, Set, Eq.mp, Metric.uniformContinuousOn_iff, Exists.intro, Min.min and 82 more
126 instances, coercions and auxiliary constants left out.

Tactic trace: 23 steps
Open to load the checked before-and-after goal states.
```
lemma Function.Periodic.uniformContinuous_of_continuous {f : ℝ → ℂ} {T : ℝ} (hT : 0 < T)
    (hp : Function.Periodic f T) (hc : ContinuousOn f (Set.Icc (-T) (2 * T))) :
    UniformContinuous f := by
…
```
Mentions: T
lemma fourier_uniformContinuous line 210 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, UniformContinuous, Real, Complex, ContinuousMap, AddCircle, HMul.hMul, OfNat.ofNat, Nat, Real.pi, AddSubgroup.zmultiples, fourier
Proof uses: Function.Periodic.uniformContinuous_of_continuous, Real.two_pi_pos, fourier_periodic, Continuous.continuousOn, Set.Icc, Neg.neg, Eq.mpr, Continuous, Complex.exp, HDiv.hDiv, Complex.I, id, Eq, congrArg, funext, Membership.mem, Submonoid, Submonoid.unitSphere, AddCircle.toCircle, HSMul.hSMul and 10 more
83 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma partialFourierSum_uniformContinuous line 215 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Complex, Nat, UniformContinuous, partialFourierSum
Proof uses: Function.Periodic.uniformContinuous_of_continuous, HMul.hMul, OfNat.ofNat, Real.pi, Real.two_pi_pos, partialFourierSum_periodic, Continuous.continuousOn, Set.Icc, Neg.neg, continuous_finsetSum, Int, fourierCoeffOn, ContinuousMap, AddCircle, AddSubgroup.zmultiples, fourier, Finset.Icc, Membership.mem, Finset, Eq.mpr and 25 more
93 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma partialFourierSum_measurable line 221 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Complex, Nat, Measurable, partialFourierSum
Proof uses: Continuous.measurable, UniformContinuous.continuous, partialFourierSum_uniformContinuous
15 instances, coercions and auxiliary constants left out.
theorem strictConvexOn_cos_Icc line 224 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: StrictConvexOn, Real, Set.Icc, HDiv.hDiv, Real.pi, OfNat.ofNat, Nat, HAdd.hAdd, Real.cos
Proof uses: strictConvexOn_of_deriv2_pos, convex_Icc, Real.continuousOn_cos, Membership.mem, Set, interior, of_eq_true, LT.lt, Nat.iterate, deriv, Eq.trans, True, Neg.neg, congrArg, Function.comp, congrFun', Function.iterate_one, Real.sin, Real.deriv_cos', congrFun and 9 more
108 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma lower_secant_bound_aux line 229 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LT.lt, OfNat.ofNat, LE.le, HSub.hSub, HMul.hMul, Nat, Real.pi, HDiv.hDiv, Norm.norm, Complex, Complex.exp, Complex.I
Proof uses: Trans.trans, Real.sqrt, HPow.hPow, Real.cos, Eq, HAdd.hAdd, rfl, mul_le_mul_of_nonneg_left, le_of_lt, div_pos, Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Bool, Nat.ble, Real.pi_pos, Eq.mpr, inferInstance, CommGroupWithZero and 195 more
220 instances, coercions and auxiliary constants left out.

Tactic trace: 34 steps
Open to load the checked before-and-after goal states.
lemma lower_secant_bound' line 260 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LE.le, abs, HSub.hSub, HMul.hMul, OfNat.ofNat, Nat, Real.pi, HDiv.hDiv, Norm.norm, Complex, Complex.exp, Complex.I
Proof uses: dite, Trans.trans, Eq, rfl, mul_nonpos_of_nonneg_of_nonpos, div_nonneg, zero_le_two, LT.lt.le, Real.pi_pos, norm_nonneg, Not, Or, Classical.em, Real.sqrt, HPow.hPow, Real.sin, HAdd.hAdd, mul_le_mul_of_nonneg_left, le_of_lt, div_pos and 218 more
254 instances, coercions and auxiliary constants left out.

Tactic trace: 56 steps
Open to load the checked before-and-after goal states.
lemma lower_secant_bound Slightly weaker version of Lemma 11..1.9 (lower secant bound) with simplified constant line 306 source
Source comment
Slightly weaker version of Lemma 11..1.9 (lower secant bound) with simplified constant.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Membership.mem, Set, Set.Icc, HAdd.hAdd, HMul.hMul, Neg.neg, OfNat.ofNat, Nat, Real.pi, HSub.hSub, LE.le, abs, HDiv.hDiv, Norm.norm, Complex, Complex.exp, Complex.I
Proof uses: dite, LT.lt, Trans.trans, Eq, rfl, le_of_not_gt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, inferInstance, AddMonoidWithOne, Mathlib.Meta.NormNum.instAtLeastTwo, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HPow.hPow, Nat.rawCast, Int.rawCast, Ring, Int.negOfNat, Mathlib.Tactic.Ring.Common.sub_congr and 132 more
173 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
```
lemma lower_secant_bound {η : ℝ} {x : ℝ} (xIcc : x ∈ Set.Icc (-2 * π + η) (2 * π - η)) (xAbs : η ≤ |x|) :
    η / 2 ≤ ‖(1 - Complex.exp (Complex.I * x))‖ := by
…
```