Carleson/Discrete/MainTheorem.lean

GitHub source file

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

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

4 declarations, 0 contain sorry, 0 declared as axioms

Proposition 2.0.2

Imports (3)
Imported by 2 files
  1. def C2_0_2 The constant used in Proposition 2.0.2 line 18 source

    Source documentation

    The constant used in Proposition 2.0.2. Has value 2 ^ (442 * a ^ 3) / (q - 1) ^ 5 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.

    noncomputable def C2_0_2 (a : ℕ) (q : ℝ≥0) : ℝ≥0 :=
…
  2. lemma le_C2_0_2 line 21 source

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

    Statement uses: Nat, LE.le, OfNat.ofNat, NNReal, Membership.mem, Set, Set.Ioc, HAdd.hAdd, C5_1_2, C5_1_3, C2_0_2

    Proof uses: LT.lt, HSub.hSub, tsub_pos_of_lt, And.left, Eq.mpr, HDiv.hDiv, HPow.hPow, HMul.hMul, 𝕔, id, Eq, GE.ge, pow_le_pow_of_le_one, LT.lt.le, congrArg, propext, tsub_le_iff_left, eq_of_heq, LE, HEq and 65 more

    124 instances, coercions and auxiliary constants left out.

    Tactic trace: 17 steps

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

  3. lemma C2_0_2_pos line 39 source

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, LT.lt, NNReal, OfNat.ofNat, C2_0_2, nnq

    Proof uses: LT.lt.trans_le, HAdd.hAdd, C5_1_2, C5_1_3, add_pos, C5_1_2_pos, C5_1_3_pos, le_C2_0_2, KernelProofData.four_le_a, ProofData.q_mem_Ioc

    28 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  4. theorem discrete_carleson line 44 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, Exists, And, MeasurableSet, LE.le, ENNReal and 19 more

    Proof uses: G', Neg.neg, exceptional_set, Exists.intro, And.intro, measurable_G', ENNReal.mul_le_of_le_div', Eq.mp, HDiv.hDiv, congrArg, Eq.symm, ENNReal.div_eq_inv_mul, zpow_neg_one, Trans.trans, HAdd.hAdd, C5_1_2, C5_1_3, 𝔓₁, Compl.compl, Eq and 37 more

    182 instances, coercions and auxiliary constants left out.

    Tactic trace: 16 steps

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