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

18 declarations, 0 contain sorry, 0 declared as axioms

Helper lemmas for the RCLike component decomposition norm bounds

Imports (1)

Carleson.ToMathlib.ENorm

Imported by 2 files

def RCLike.Components TODO: check whether this is the right approach line 18 source
Source documentation
TODO: check whether this is the right approach

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: RCLike, Finset
Proof uses: Insert.insert, OfNat.ofNat, Neg.neg, RCLike.I, Singleton.singleton
18 instances, coercions and auxiliary constants left out.
```
def Components {𝕂 : Type*} [RCLike 𝕂] : Finset 𝕂 := {1, -1, RCLike.I, -RCLike.I}
```
lemma RCLike.Components.norm_eq_one line 20 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: RCLike, Membership.mem, Finset, RCLike.Components, Ne, OfNat.ofNat, Eq, Real, Norm.norm
Proof uses: Or, Neg.neg, RCLike.I, Eq.mp, Insert.insert, Singleton.singleton, Eq.trans, congrArg, Eq.mpr, id, of_eq_true, True, congrFun', NormOneClass.norm_one, eq_self, norm_neg, RCLike.norm_I_of_ne_zero, Eq.symm, Eq.refl, propext and 1 more
57 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
lemma RCLike.Components.norm_le_one line 32 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: RCLike, Membership.mem, Finset, RCLike.Components, LE.le, Real, Norm.norm, OfNat.ofNat
Proof uses: dite, Eq, Eq.mpr, id, congrArg, of_eq_true, Eq.trans, True, congrFun', norm_zero, Not, RCLike.Components.norm_eq_one, le_refl
34 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
def RCLike.component TODO: check whether this is the right approach line 42 source
Source documentation
TODO: check whether this is the right approach

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: RCLike, NNReal
Proof uses: Real.toNNReal, AddMonoidHom, Real, AddZero.mk, AddMonoid.toZero, RCLike.re, HMul.hMul, RingHom, starRingEnd
26 instances, coercions and auxiliary constants left out.
```
def component {𝕂 : Type*} [RCLike 𝕂] (c : 𝕂) (a : 𝕂) : ℝ≥0 :=
…
```
Mentions: c
lemma RCLike.component_le_norm line 45 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: RCLike, Membership.mem, Finset, RCLike.Components, LE.le, Real, RCLike.component, Norm.norm
Proof uses: id, Eq.mpr, Real.toNNReal, AddMonoidHom, AddZero.mk, AddMonoid.toZero, RCLike.re, HMul.hMul, RingHom, starRingEnd, Max.max, OfNat.ofNat, Eq, congrArg, Real.coe_toNNReal', max_le, LE.le.trans, RCLike.re_le_norm, congrFun', Eq.trans and 8 more
65 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma RCLike.component_le_nnnorm line 56 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: RCLike, Membership.mem, Finset, RCLike.Components, LE.le, NNReal, RCLike.component, NNNorm.nnnorm
Proof uses: Eq.mpr, Real.toNNReal, Norm.norm, id, Eq, congrArg, Eq.symm, norm_toNNReal, NNReal.le_toNNReal_of_coe_le, RCLike.component_le_norm
29 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma RCLike.decomposition line 62 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: RCLike, Eq, HAdd.hAdd, HMul.hMul, OfNat.ofNat, RingHom, Real, Algebra.algebraMap, RCLike.component, Neg.neg, RCLike.I
Proof uses: id, Eq.mpr, Real.toNNReal, AddMonoidHom, AddZero.mk, AddMonoid.toZero, RCLike.re, starRingEnd, Max.max, RCLike.im, congrFun', congrArg, congr, Eq.trans, NNReal, map_one, mul_one, one_mul, map_neg, NNRat and 19 more
153 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
theorem RCLike.nnnorm_ofReal line 74 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: RCLike, NNReal, Eq, NNNorm.nnnorm
Proof uses: NNReal.eq, of_eq_true, Real, Eq.trans, True, congrArg, RingHom, Algebra.algebraMap, nnnorm_algebraMap', NNReal.nnnorm_eq, eq_self
38 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem RCLike.enorm_ofReal line 80 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: RCLike, NNReal, Eq, ENNReal, ENorm.enorm
Proof uses: Eq.mpr, id, congrFun', congrArg, enorm_NNReal, NNNorm.nnnorm, enorm_eq_nnnorm, of_eq_true, Eq.trans, True, RingHom, Real, Algebra.algebraMap, nnnorm_algebraMap', NNReal.nnnorm_eq, eq_self
53 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma RCLike.component_one_add_neg_one line 122 source
lemma RCLike.component_I_add_neg_I line 131 source

lemma RCLike.norm_realPart_le Norm of the real component part is at most ‖a‖ line 143 source

Source documentation

Norm of the real component part is at most ‖a‖.

private lemma norm_realPart_le {𝕂 : Type*} [RCLike 𝕂] (a : 𝕂) :
    ‖algebraMap ℝ 𝕂 (component 1 a).toReal +
      (-1 : 𝕂) * algebraMap ℝ 𝕂 (component (-1) a).toReal‖ ≤ ‖a‖ := by
…

Mentions: RCLike.component

lemma RCLike.norm_imPart_le Norm of the imaginary component part is at most ‖a‖ line 150 source

Source documentation

Norm of the imaginary component part is at most ‖a‖.

private lemma norm_imPart_le {𝕂 : Type*} [RCLike 𝕂] (a : 𝕂) :
    ‖(I : 𝕂) * algebraMap ℝ 𝕂 (component I a).toReal +
      (-I : 𝕂) * algebraMap ℝ 𝕂 (component (-I) a).toReal‖ ≤ ‖a‖ := by
…

Mentions: RCLike.component

lemma RCLike.norm_posReal_le max(re a, 0) embedded in 𝕂 has norm at most |re a| line 164 source

Source documentation

max(re a, 0) embedded in 𝕂 has norm at most |re a|.

private lemma norm_posReal_le {𝕂 : Type*} [RCLike 𝕂] (a : 𝕂) :
    ‖(algebraMap ℝ 𝕂 (component 1 a).toReal : 𝕂)‖ ≤
      ‖algebraMap ℝ 𝕂 (component 1 a).toReal +
        (-1 : 𝕂) * algebraMap ℝ 𝕂 (component (-1) a).toReal‖ := by
…

Mentions: RCLike.component

lemma RCLike.norm_negReal_le max(-re a, 0) negated and embedded in 𝕂 has norm at most |re a| line 175 source

Source documentation

max(-re a, 0) negated and embedded in 𝕂 has norm at most |re a|.

private lemma norm_negReal_le {𝕂 : Type*} [RCLike 𝕂] (a : 𝕂) :
    ‖(-1 : 𝕂) * algebraMap ℝ 𝕂 (component (-1) a).toReal‖ ≤
      ‖algebraMap ℝ 𝕂 (component 1 a).toReal +
        (-1 : 𝕂) * algebraMap ℝ 𝕂 (component (-1) a).toReal‖ := by
…

Mentions: RCLike.component

lemma RCLike.norm_posIm_le I * max(im a, 0) has norm at most ‖I * im⁺ - I * im⁻‖ line 187 source

Source documentation

I * max(im a, 0) has norm at most ‖I * im⁺ - I * im⁻‖.

private lemma norm_posIm_le {𝕂 : Type*} [RCLike 𝕂] (a : 𝕂) :
    ‖(I : 𝕂) * algebraMap ℝ 𝕂 (component I a).toReal‖ ≤
      ‖(I : 𝕂) * algebraMap ℝ 𝕂 (component I a).toReal +
        (-I : 𝕂) * algebraMap ℝ 𝕂 (component (-I) a).toReal‖ := by
…

Mentions: RCLike.component

lemma RCLike.norm_negIm_le -I * max(-im a, 0) has norm at most ‖I * im⁺ - I * im⁻‖ line 201 source

Source documentation

-I * max(-im a, 0) has norm at most ‖I * im⁺ - I * im⁻‖.

private lemma norm_negIm_le {𝕂 : Type*} [RCLike 𝕂] (a : 𝕂) :
    ‖(-I : 𝕂) * algebraMap ℝ 𝕂 (component (-I) a).toReal‖ ≤
      ‖(I : 𝕂) * algebraMap ℝ 𝕂 (component I a).toReal +
        (-I : 𝕂) * algebraMap ℝ 𝕂 (component (-I) a).toReal‖ := by
…

Mentions: RCLike.component

theorem RCLike.induction TODO: clean up the proof line 217 source

Source comment

TODO: clean up the proof

standard axioms: Classical.choice, Quot.sound, propext what this means

Statement uses: RCLike, Mul, HAdd.hAdd, Membership.mem, Finset, RCLike.Components, Function.comp, Real, RingHom, Algebra.algebraMap, NNReal, RCLike.component, HSMul.hSMul, LE.le, Norm.norm, HMul.hMul

Proof uses: Eq, OfNat.ofNat, Neg.neg, RCLike.I, funext, id, RCLike.decomposition, Eq.mpr, congrArg, Eq.symm, add_assoc, congr_fun, Eq.mp, congrFun', one_mul, congr, of_eq_true, Insert.insert, Singleton.singleton, Eq.trans and 5 more

104 instances, coercions and auxiliary constants left out.

Tactic trace: 103 steps

Open to load the checked before-and-after goal states.

theorem induction {α : Type*} {𝕂 : Type*} [RCLike 𝕂]
  {β : Type*} [Mul β] {a b}
  {P : (α → 𝕂) → Prop}
  (P_add : ∀ {f g : α → 𝕂}, P f → P g → P (f + g))
  (P_components : ∀ {f : α → 𝕂} {c : 𝕂} (_ : c ∈ RCLike.Components),
    P f → P (algebraMap ℝ 𝕂 ∘ NNReal.toReal ∘ RCLike.component c ∘ f))
  (P_mul_unit : ∀ {f : α → 𝕂} {c : 𝕂} (_ : c ∈ RCLike.Components), P f → P (c • f))
  {motive : (α → 𝕂) → β → Prop}
  (motive_nnreal : ∀ {f : α → ℝ≥0} (_ : P (algebraMap ℝ 𝕂 ∘ NNReal.toReal ∘ f)),
    motive (algebraMap ℝ 𝕂 ∘ NNReal.toReal ∘ f) a)
  (motive_add' : ∀ {n : β} {f g : α → 𝕂} (_ : ∀ {x}, ‖f x‖ ≤ ‖f x + g x‖)
    (_ : ∀ {x}, ‖g x‖ ≤ ‖f x + g x‖) (_ : P f) (_ : P g),
…

Mentions: g, c, RCLike.Components, RCLike.component