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

6 declarations, 0 contain sorry, 0 declared as axioms

Imports (1)

Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap

Imported by 4 files

lemma starRingEnd_div_mul_eq_norm line 13 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: RCLike, Eq, HMul.hMul, RingHom, starRingEnd, HDiv.hDiv, Norm.norm
Proof uses: Eq.mpr, Inv.inv, HPow.hPow, Nat, OfNat.ofNat, id, congrFun', congrArg, Eq.trans, div_eq_inv_mul, map_mul, map_inv₀, RCLike.conj_ofReal, mul_assoc, RCLike.conj_mul, Real, congr, Ne, Or, eq_or_ne and 40 more
124 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma enorm_algebraMap' move to Mathlib.Analysis.Normed.Module.Basic, next to nnnorm_algebraMap' line 22 source
Source comment
move to Mathlib.Analysis.Normed.Module.Basic, next to nnnorm_algebraMap'

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedField, SeminormedRing, NormedAlgebra, NormOneClass, Eq, ENNReal, ENorm.enorm, RingHom, Algebra.algebraMap
Proof uses: of_eq_true, NNNorm.nnnorm, Eq.trans, True, congrFun', congrArg, NNReal, nnnorm_algebraMap', eq_self
54 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma enorm_algebraMap' {𝕜 : Type*} (𝕜' : Type*) [NormedField 𝕜] [SeminormedRing 𝕜']
    [NormedAlgebra 𝕜 𝕜'] [NormOneClass 𝕜'] (x : 𝕜) : ‖(algebraMap 𝕜 𝕜') x‖ₑ = ‖x‖ₑ := by
…
```
lemma enorm_integral_norm_eq_integral_enorm line 26 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, RCLike, MeasureTheory.Measure, MeasureTheory.Integrable, Eq, ENNReal, ENorm.enorm, Real, MeasureTheory.integral, Norm.norm, MeasureTheory.lintegral
Proof uses: id, Eq.mpr, NNNorm.nnnorm, ENNReal.ofReal, congrArg, MeasureTheory.lintegral_coe_eq_integral, MeasureTheory.Integrable.norm, NNReal, Real.toNNReal, abs, Iff.mpr, LE.le, OfNat.ofNat, abs_eq_self, MeasureTheory.integral_nonneg, norm_nonneg, NNReal.eq, of_eq_true, Eq.trans, True and 3 more
83 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma enorm_integral_starRingEnd_mul_eq_lintegral_enorm line 36 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: RCLike, MeasurableSpace, MeasureTheory.Measure, MeasureTheory.Integrable, Eq, ENNReal, ENorm.enorm, MeasureTheory.integral, Real, HMul.hMul, RingHom, starRingEnd, HDiv.hDiv, Norm.norm, MeasureTheory.lintegral
Proof uses: Eq.mpr, id, congrFun', congrArg, funext, starRingEnd_div_mul_eq_norm, integral_ofReal, enorm_algebraMap', of_eq_true, Eq.trans, True, enorm_integral_norm_eq_integral_enorm, eq_self
84 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma enorm_integral_mul_starRingEnd_comm line 43 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: RCLike, MeasurableSpace, MeasureTheory.Measure, Eq, ENNReal, ENorm.enorm, MeasureTheory.integral, Real, HMul.hMul, RingHom, starRingEnd
Proof uses: Eq.mpr, id, congrArg, Eq.symm, RCLike.enorm_conj, integral_conj, eq_of_heq, ENorm, HEq, Eq.refl, HEq.refl, NormedAddCommGroup, NormedSpace, funext, of_eq_true, Eq.trans, True, congrFun', map_mul, RingHomCompTriple.comp_apply and 3 more
81 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
theorem MeasureTheory.setIntegral_union_2 line 55 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, NormedAddCommGroup, NormedSpace, Real, Set, MeasureTheory.Measure, Disjoint, MeasurableSet, MeasureTheory.IntegrableOn, Union.union, Eq, MeasureTheory.integral, MeasureTheory.Measure.restrict, HAdd.hAdd
Proof uses: MeasureTheory.setIntegral_union, MeasureTheory.IntegrableOn.left_of_union, MeasureTheory.IntegrableOn.right_of_union
40 instances, coercions and auxiliary constants left out.