Documentation

Carleson.Antichain.Basic

6.1. The density arguments #

This file contains the proofs of lemmas 6.1.1, 6.1.2 and 6.1.3 from the blueprint.

Main results #

source
def ShortVariables.termNnqt :
Lean.ParserDescr

$\tilde{q}$ from definition 6.1.10, as a nonnegative real number. Note that (nnqt : ℝ)⁻¹ - 2⁻¹ = 2⁻¹ * q⁻¹.

Equations
Instances For
    source
    theorem inv_nnqt_eq {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] :
    (2 * ↑(nnq X) / (↑(nnq X) + 1))⁻¹ = 2⁻¹ + 2⁻¹ * q⁻¹
    source
    theorem inv_nnqt_mem_Ico {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] :
    (2 * ↑(nnq X) / (↑(nnq X) + 1))⁻¹ ∈ Set.Ico (3 / 4) 1
    source
    theorem one_lt_nnqt {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] :
    1 < 2 * nnq X / (nnq X + 1)
    source
    theorem one_lt_nnqt_coe {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] :
    1 < 2 * ↑(nnq X) / (↑(nnq X) + 1)
    source
    theorem nnqt_lt_nnq {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] :
    2 * nnq X / (nnq X + 1) < nnq X
    source
    theorem nnqt_lt_nnq_coe {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] :
    2 * ↑(nnq X) / (↑(nnq X) + 1) < ↑(nnq X)
    source
    theorem nnqt_lt_two {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] :
    2 * nnq X / (nnq X + 1) < 2
    source
    theorem nnqt_lt_two_coe {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] :
    2 * ↑(nnq X) / (↑(nnq X) + 1) < 2
    source
    theorem tile_disjointness {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {𝔄 : Set (𝔓 X)} (h𝔄 : IsAntichain (fun (x1 x2 : 𝔓 X) => x1 ≀ x2) 𝔄) {p p' : 𝔓 X} (hp : p ∈ 𝔄) (hp' : p' ∈ 𝔄) (hE : Β¬Disjoint (E p) (E p')) :
    p = p'

    Lemma 6.1.1.

    source
    noncomputable def C6_1_2 (a : β„•) :
    β„•

    Constant appearing in Lemma 6.1.2. Has value 2 ^ (102 * a ^ 3) in the blueprint.

    Equations
    Instances For
      source
      theorem C6_1_2_ne_zero (a : β„•) :
      ↑(C6_1_2 a) β‰  0
      source
      theorem norm_Ks_le' {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {x y : X} {𝔄 : Set (𝔓 X)} (p : ↑𝔄) (hxE : x ∈ E ↑p) (hy : Ks (𝔰 ↑p) x y β‰  0) :
      β€–Ks (𝔰 ↑p) x yβ€–β‚‘ ≀ 2 ^ (6 * a + (𝕔 + 1) * a ^ 3) / MeasureTheory.volume (Metric.ball (𝔠 ↑p) (8 * ↑(defaultD a) ^ 𝔰 ↑p))
      source
      theorem maximal_bound_antichain {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {𝔄 : Set (𝔓 X)} (h𝔄 : IsAntichain (fun (x1 x2 : 𝔓 X) => x1 ≀ x2) 𝔄) {f : X β†’ β„‚} (hfm : Measurable f) (x : X) :
      β€–carlesonSum 𝔄 f xβ€–β‚‘ ≀ ↑(C6_1_2 a) * maximalFunction MeasureTheory.volume 𝔄 𝔠 (fun (𝔭 : 𝔓 X) => 8 * ↑(defaultD a) ^ 𝔰 𝔭) 1 f x

      Lemma 6.1.2.

      source
      noncomputable def C6_1_3 (a : β„•) (q : NNReal) :
      NNReal

      Constant appearing in Lemma 6.1.3. Has value 2 ^ (103 * a ^ 3) in the blueprint.

      Equations
      Instances For
        source
        noncomputable def Lemma6_1_3.π“œ {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] (𝔄 : Set (𝔓 X)) (u : X β†’ β„‚) (x : X) :
        ENNReal

        The maximal function used in the proof of Lemma 6.1.3

        Equations
        Instances For
          source
          noncomputable def Lemma6_1_3.qt (X : Type u_1) {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] :
          ℝ

          $\tilde{q}$ from definition 6.1.10, as a real number.

          Equations
          Instances For
            source
            theorem Lemma6_1_3.inv_qt_eq (X : Type u_1) {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] :
            (qt X)⁻¹ = 2⁻¹ + 2⁻¹ * q⁻¹
            source
            noncomputable def Lemma6_1_3.p (X : Type u_1) {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] :
            ℝ

            Exponent used for the application of HΓΆlder's inequality in the proof of Lemma 6.1.3.

            Equations
            Instances For
              source
              theorem Lemma6_1_3.inv_p_eq (X : Type u_1) {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] :
              (p X)⁻¹ = 3 / 2 - (qt X)⁻¹
              source
              theorem Lemma6_1_3.inv_p_eq' (X : Type u_1) {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] :
              (p X)⁻¹ = 1 - 2⁻¹ * q⁻¹
              source
              theorem Lemma6_1_3.p_pos (X : Type u_1) {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] :
              0 < p X
              source
              theorem Lemma6_1_3.one_lt_p (X : Type u_1) {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] :
              1 < p X
              source
              theorem Lemma6_1_3.p_lt_two (X : Type u_1) {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] :
              p X < 2
              source
              noncomputable def Lemma6_1_3.π“œp {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] (𝔄 : Set (𝔓 X)) (p : ℝ) (u : X β†’ β„‚) (x : X) :
              ENNReal

              The p maximal function used in the proof.

              Equations
              Instances For
                source
                theorem Lemma6_1_3.eLpNorm_π“œp_le {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] (𝔄 : Set (𝔓 X)) {f : X β†’ β„‚} (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) :
                MeasureTheory.eLpNorm (π“œp 𝔄 (p X) f) 2 MeasureTheory.volume ≀ ↑(C2_0_6 (↑(defaultA a)) (p X).toNNReal 2) * MeasureTheory.eLpNorm f 2 MeasureTheory.volume

                Maximal function bound needed in the proof

                source
                theorem Lemma6_1_3.eLpNorm_π“œ_le_eLpNorm_π“œp_mul {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] (𝔄 : Set (𝔓 X)) {f : X β†’ β„‚} (hf : Measurable f) (hfF : βˆ€ (x : X), β€–f xβ€– ≀ F.indicator 1 x) {p p' : ℝ} (hpp : p.HolderConjugate p') :
                MeasureTheory.eLpNorm (π“œ 𝔄 f) 2 MeasureTheory.volume ≀ densβ‚‚ 𝔄 ^ p'⁻¹ * MeasureTheory.eLpNorm (π“œp 𝔄 p f) 2 MeasureTheory.volume

                A maximal function bound via an application of H"older's inequality

                source
                theorem Lemma6_1_3.const_check {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] :
                ↑(C6_1_2 a) * C2_0_6 (↑(defaultA a)) (p X).toNNReal 2 ≀ C6_1_3 a (nnq X)

                Tedious check that the constants work out.

                source
                theorem dens2_antichain {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {𝔄 : Set (𝔓 X)} (h𝔄 : IsAntichain (fun (x1 x2 : 𝔓 X) => x1 ≀ x2) 𝔄) {f : X β†’ β„‚} (hfF : βˆ€ (x : X), β€–f xβ€– ≀ F.indicator 1 x) (hf : Measurable f) {g : X β†’ β„‚} (hgG : βˆ€ (x : X), β€–g xβ€– ≀ G.indicator 1 x) (hg : Measurable g) :
                β€–βˆ« (x : X), (starRingEnd β„‚) (g x) * carlesonSum 𝔄 f xβ€–β‚‘ ≀ ↑(C6_1_3 a (nnq X)) * densβ‚‚ 𝔄 ^ ((2 * ↑(nnq X) / (↑(nnq X) + 1))⁻¹ - 2⁻¹) * MeasureTheory.eLpNorm f 2 MeasureTheory.volume * MeasureTheory.eLpNorm g 2 MeasureTheory.volume

                Lemma 6.1.3 (inequality 6.1.11).