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

15 declarations, 0 contain sorry, 0 declared as axioms

6. Proof of the Antichain Operator Proposition

This file contains the proofs of Lemma 6.1.4 and Proposition 2.0.3 from the blueprint. Three versions of the latter are provided.

Main results

dens1_antichain : Lemma 6.1.4.
antichain_operator: Proposition 2.0.3.

Imports (3)

Imported by 2 files

lemma dens1_antichain_rearrange line 30 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, MeasureTheory.BoundedCompactSupport, MeasureTheory.MeasureSpace.volume, LE.le, ENNReal and 17 more
Proof uses: Trans.trans, Eq, HAdd.hAdd, LT.lt, Eq.mpr, id, congrArg, MeasureTheory.eLpNorm_two_eq_enorm_integral_mul_conj, MeasureTheory.BoundedCompactSupport.memLp, MeasureTheory.BoundedCompactSupport.adjointCarlesonSum, eq_of_heq, ENorm, HEq, Eq.refl, HEq.refl, Eq.symm, NormedAddCommGroup, NormedSpace, MeasurableSpace, MeasureTheory.Measure and 48 more
210 instances, coercions and auxiliary constants left out.

Tactic trace: 35 steps
Open to load the checked before-and-after goal states.
def dach h(p) in the proof of Lemma 6.1.4 (dens₁ antichain h) line 86 source
Source documentation
h(p) in the proof of Lemma 6.1.4 (dens₁ antichain h).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, ENNReal
Proof uses: HMul.hMul, Inv.inv, MeasureTheory.Measure, MeasureTheory.MeasureSpace.volume, Metric.ball, 𝔠, OfNat.ofNat, HPow.hPow, 𝔰, MeasureTheory.lintegral, Finset.sum, Finset.filter, And, Membership.mem, LE.le, 𝓘, Classical.propDecidable, Finset.univ, HAdd.hAdd, EDist.edist and 7 more
87 instances, coercions and auxiliary constants left out.
```
def dach (𝔄 : Set (𝔓 X)) (p : 𝔓 X) (g : X → ℂ) : ℝ≥0∞ :=
…
```
Mentions: 𝔓, g
lemma dens1_antichain_dach line 92 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, Measurable, LE.le, Norm.norm, Set.indicator and 19 more
Proof uses: MeasureTheory.BoundedCompactSupport, bcs_of_measurable_of_le_indicator_g, Trans.trans, Eq, Inv.inv, MeasureTheory.Measure, Metric.ball, 𝔠, 𝔰, And, 𝓘, EDist.edist, WithFunctionDistance, HDiv.hDiv, PreTileStructure.𝒬, Neg.neg, MeasureTheory.integral, adjointCarleson, RingHom, starRingEnd and 103 more
251 instances, coercions and auxiliary constants left out.

Tactic trace: 39 steps
Open to load the checked before-and-after goal states.
def M14 The maximalFunction instance that appears in Lemma 6.1.4's proof line 146 source
Source documentation
The maximalFunction instance that appears in Lemma 6.1.4's proof.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, ENNReal
Proof uses: maximalFunction, MeasureTheory.MeasureSpace.volume, 𝔠, HMul.hMul, OfNat.ofNat, HPow.hPow, 𝔰
49 instances, coercions and auxiliary constants left out.
```
def M14 (𝔄 : Set (𝔓 X)) (p : ℝ) (g : X → ℂ) : X → ℝ≥0∞ :=
…
```
Mentions: 𝔓, g
lemma eLpNorm_le_M14 line 149 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, Membership.mem, Metric.ball, 𝔠, HMul.hMul and 14 more
Proof uses: Metric.measure_ball_pos, id, mul_pos, 𝕔, Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Bool, Nat.ble, zpow_pos, Iff.mpr, Nat.cast_pos', pow_pos, inferInstance, PartialOrder, Eq.mpr, Eq, congrArg, mul_comm and 57 more
206 instances, coercions and auxiliary constants left out.

Tactic trace: 25 steps
Open to load the checked before-and-after goal states.
lemma dach_bound Equations (6.1.34) to (6.1.37) in Lemma 6.1.4 line 174 source
Source documentation
Equations (6.1.34) to (6.1.37) in Lemma 6.1.4.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, IsAntichain, LE.le, Membership.mem, Measurable and 16 more
Proof uses: id, Eq.mpr, MeasureTheory.Measure, MeasureTheory.MeasureSpace.volume, MeasureTheory.lintegral, Finset.sum, Finset.filter, And, 𝓘, Classical.propDecidable, Finset.univ, HAdd.hAdd, EDist.edist, WithFunctionDistance, HDiv.hDiv, PreTileStructure.𝒬, Neg.neg, E, ENorm.enorm, Eq and 110 more
293 instances, coercions and auxiliary constants left out.

Tactic trace: 64 steps
Open to load the checked before-and-after goal states.
```
lemma dach_bound (h𝔄 : IsAntichain (· ≤ ·) 𝔄) {p : 𝔓 X} (mp : p ∈ 𝔄) (hg : Measurable g)
    (hgG : ∀ x, ‖g x‖ ≤ G.indicator 1 x) {x₀ : X} (hx : x₀ ∈ ball (𝔠 p) (14 * D ^ 𝔰 p)) :
    dach 𝔄 p g ≤ C6_1_6 a * dens₁ 𝔄 ^ (p₆ a : ℝ)⁻¹ * M14 𝔄 (q₆ a) g x₀ := by
…
```
Mentions: 𝔓, g, 𝔠, 𝔰, dach, dens₁, M14
lemma M14_bound line 232 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, MeasureTheory.MemLp, OfNat.ofNat, ENNReal, MeasureTheory.MeasureSpace.volume and 7 more
Proof uses: KernelProofData.four_le_a, MeasureTheory.HasStrongType, Real.toNNReal, C2_0_6, hasStrongType_maximalFunction, 𝔠, 𝔰, Iff.mpr, LT.lt, Real.toNNReal_pos, LT.lt.trans, zero_lt_one, Antichain.one_lt_q₆, Eq.mpr, id, Eq, LE.le.trans_lt, HDiv.hDiv, Antichain.q₆_le_superparticular, Mathlib.Meta.NormNum.isNNRat_lt_true and 26 more
160 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
lemma le_C6_1_4 line 250 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, NNReal, HMul.hMul, Tile.C6_1_5, HPow.hPow, HAdd.hAdd, Antichain.C6_1_6, C6_1_4
Proof uses: id, 𝕔, HDiv.hDiv, Eq.mpr, Eq, congrArg, congrFun', C6_1_4_def, Eq.trans, pow_le_pow_right₀, one_le_two, LE.le.trans_eq, mul_le_mul_of_nonneg_right, Nat.zero_le, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat and 78 more
129 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
lemma dens1_antichain_sq line 262 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, IsAntichain, LE.le, Measurable, Norm.norm and 11 more
Proof uses: Trans.trans, Tile.C6_1_5, HAdd.hAdd, Antichain.C6_1_6, Antichain.p₆, M14, Antichain.q₆, MeasureTheory.lintegral, ENorm.enorm, MeasureTheory.Measure.restrict, Set.iUnion, Membership.mem, E, Eq, Finset.sum, Finset.filter, Classical.propDecidable, Finset.univ, dach, dens1_antichain_dach and 123 more
232 instances, coercions and auxiliary constants left out.

Tactic trace: 39 steps
Open to load the checked before-and-after goal states.
lemma dens1_antichain Lemma 6.1.4 line 309 source
Source documentation
Lemma 6.1.4.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, IsAntichain, LE.le, Measurable, Norm.norm and 15 more
Proof uses: MeasureTheory.BoundedCompactSupport, bcs_of_measurable_of_le_indicator_f, bcs_of_measurable_of_le_indicator_g, Trans.trans, adjointCarlesonSum, MeasureTheory.lintegral, Eq.mpr, id, Eq, congrArg, adjointCarlesonSum_adjoint, Eq.rec, Eq.refl, funext, Eq.trans, Eq.symm, RCLike.enorm_conj, enorm_mul, MeasureTheory.enorm_integral_le_lintegral_enorm, MeasureTheory.eLpNorm_enorm and 23 more
181 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
```
lemma dens1_antichain (h𝔄 : IsAntichain (· ≤ ·) 𝔄) (hf : Measurable f)
    (hfF : ∀ x, ‖f x‖ ≤ F.indicator 1 x) (hg : Measurable g) (hgG : ∀ x, ‖g x‖ ≤ G.indicator 1 x) :
    ‖∫ x, conj (g x) * carlesonSum 𝔄 f x‖ₑ ≤
      C6_1_4 a * dens₁ 𝔄 ^ (8 * a ^ 4 : ℝ)⁻¹ * eLpNorm f 2 volume * eLpNorm g 2 volume := by
…
```
Mentions: g, carlesonSum, dens₁
def C2_0_3 The constant appearing in Proposition 2.0.3 line 332 source
Source documentation
The constant appearing in Proposition 2.0.3. Has value 2 ^ (117 * a ^ 3) in the blueprint.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NNReal
Proof uses: HDiv.hDiv, HPow.hPow, OfNat.ofNat, HMul.hMul, HAdd.hAdd, 𝕔, HSub.hSub
24 instances, coercions and auxiliary constants left out.
```
def C2_0_3 (a : ℕ) (q : ℝ≥0) : ℝ≥0 := 2 ^ ((𝕔 + 5 + 𝕔 / 8) * a ^ 3) / (q - 1)
…
```
lemma ineq_aux_2_0_3 line 336 source
theorem antichain_operator Proposition 2.0.3 line 362 source
Source documentation
Proposition 2.0.3.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, IsAntichain, LE.le, Measurable, Norm.norm and 19 more
Proof uses: Eq, rfl, Eq.mpr, Int.subNatNat, id, Eq.trans, congr, congrArg, Eq.symm, Nat.cast_one, congrFun', Int.cast_one, of_decide_eq_true, Bool, Decidable.decide, Bool.true, Eq.refl, HAdd.hAdd, Ne, propext and 128 more
293 instances, coercions and auxiliary constants left out.

Tactic trace: 49 steps
Open to load the checked before-and-after goal states.
```
theorem antichain_operator (h𝔄 : IsAntichain (· ≤ ·) 𝔄) (hf : Measurable f)
    (hf1 : ∀ x, ‖f x‖ ≤ F.indicator 1 x) (hg : Measurable g) (hg1 : ∀ x, ‖g x‖ ≤ G.indicator 1 x) :
    ‖∫ x, conj (g x) * carlesonSum 𝔄 f x‖ₑ ≤
      C2_0_3 a nnq * dens₁ 𝔄 ^ ((q - 1) / (8 * a ^ 4)) * dens₂ 𝔄 ^ (q⁻¹ - 2⁻¹) *
        eLpNorm f 2 volume * eLpNorm g 2 volume := by
…
```
Mentions: g, carlesonSum, C2_0_3, nnq, dens₁, dens₂
theorem antichain_operator' Version of the antichain operator theorem, but controlling the integral of the norm instead of the integral of the function multiplied by another function line 432 source
Source documentation
Version of the antichain operator theorem, but controlling the integral of the norm instead of the integral of the function multiplied by another function.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, IsAntichain, LE.le, Measurable, Norm.norm and 19 more
Proof uses: Eq, Ne, Or, eq_or_ne, of_eq_true, Eq.trans, True, congrFun', congrArg, div_zero, Eq.symm, div_self, Not, False, eq_false, not_false_eq_true, LE.le.trans, MeasureTheory.lintegral_mono_set, MeasureTheory.BoundedCompactSupport, bcs_of_measurable_of_le_indicator_f and 59 more
266 instances, coercions and auxiliary constants left out.

Tactic trace: 25 steps
Open to load the checked before-and-after goal states.
```
theorem antichain_operator' {A : Set X} (h𝔄 : IsAntichain (· ≤ ·) 𝔄)
    (hf : Measurable f) (hfF : ∀ x, ‖f x‖ ≤ F.indicator 1 x) (hA : A ⊆ G) :
    ∫⁻ x in A, ‖carlesonSum 𝔄 f x‖ₑ ≤
    C2_0_3 a nnq * dens₁ 𝔄 ^ ((q - 1) / (8 * a ^ 4)) * dens₂ 𝔄 ^ (q⁻¹ - 2⁻¹) *
    eLpNorm f 2 volume * volume G ^ (1/2 : ℝ) := by
…
```
Mentions: A, carlesonSum, C2_0_3, nnq, dens₁, dens₂
theorem antichain_operator_le_volume Documented declaration: antichain_operator_le_volume line 464 source
Source documentation
Version of the antichain operator theorem, but controlling the integral of the norm instead of the integral of the function multiplied by another function, and with the upper bound in terms of volume F and volume G.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, IsAntichain, LE.le, Measurable, Norm.norm and 18 more
Proof uses: LE.le.trans, MeasureTheory.eLpNorm, antichain_operator', mul_le_mul', le_refl, Trans.trans, MeasureTheory.eLpNorm_mono, le_abs_self, Eq.mpr, ENNReal.toReal, id, Eq, congrArg, MeasureTheory.eLpNorm_indicator_const, ProofData.measurableSet_F, Mathlib.Meta.NormNum.isNat_eq_false, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Nat.cast_zero and 18 more
168 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
theorem antichain_operator_le_volume {A : Set X} (h𝔄 : IsAntichain (· ≤ ·) 𝔄)
    (hf : Measurable f) (hfF : ∀ x, ‖f x‖ ≤ F.indicator 1 x) (hA : A ⊆ G) :
    ∫⁻ x in A, ‖carlesonSum 𝔄 f x‖ₑ ≤
    C2_0_3 a nnq * dens₁ 𝔄 ^ ((q - 1) / (8 * a ^ 4)) * dens₂ 𝔄 ^ (q⁻¹ - 2⁻¹) *
    volume F ^ (1/2 : ℝ) * volume G ^ (1/2 : ℝ) := by
…
```
Mentions: A, carlesonSum, C2_0_3, nnq, dens₁, dens₂