Documentation

Carleson.Antichain.AntichainTileCount

6.3. Proof of the Antichain Tile Count Lemma #

This file contains the proofs of lemmas 6.3.1, 6.3.2, 6.3.3, 6.3.4 and 6.1.6 from the blueprint.

Main results #

source
theorem Antichain.tile_reach {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} {N : β„•} {p p' : 𝔓 X} (hp : dist_{𝔠 p, ↑(defaultD a) ^ 𝔰 p / 4} (𝒬 p) Ο‘ ≀ 2 ^ N) (hp' : dist_{𝔠 p', ↑(defaultD a) ^ 𝔰 p' / 4} (𝒬 p') Ο‘ ≀ 2 ^ N) (hI : π“˜ p ≀ π“˜ p') (hs : 𝔰 p < 𝔰 p') :
smul (2 ^ (N + 2)) p ≀ smul (2 ^ (N + 2)) p'

Lemma 6.3.1.

source
def Antichain.𝔄_aux {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)) (Ο‘ : Θ X) (N : β„•) :
Set (𝔓 X)

Def 6.3.15.

Equations
Instances For
    source
    theorem Antichain.pairwiseDisjoint_𝔄_aux {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)} {Ο‘ : Θ X} :
    Set.univ.PairwiseDisjoint fun (N : β„•) => (𝔄_aux 𝔄 Ο‘ N).toFinset
    source
    theorem Antichain.biUnion_𝔄_aux {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)} {Ο‘ : Θ X} :
    βˆƒ (N : β„•), ((Finset.range N).biUnion fun (N : β„•) => (𝔄_aux 𝔄 Ο‘ N).toFinset) = 𝔄.toFinset
    source
    theorem Antichain.stack_density {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)) (Ο‘ : Θ X) (N : β„•) (L : Grid X) :
    βˆ‘ p ∈ (𝔄_aux 𝔄 Ο‘ N).toFinset with π“˜ p = L, MeasureTheory.volume (E p ∩ G) ≀ 2 ^ (a * (N + 5)) * dens₁ 𝔄 * MeasureTheory.volume ↑L

    Lemma 6.3.2.

    source
    theorem Antichain.Ep_inter_G_inter_Ip'_subset_E2 {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)} (Ο‘ : Θ X) (N : β„•) {p p' : 𝔓 X} (hpin : p ∈ (𝔄_aux 𝔄 Ο‘ N).toFinset) (hp' : Ο‘ ∈ ball_{𝔠 p', ↑(defaultD a) ^ 𝔰 p' / 4} (𝒬 p') (2 ^ (N + 1))) (hs : 𝔰 p' < 𝔰 p) (hπ“˜ : (↑(π“˜ p') ∩ ↑(π“˜ p)).Nonempty) :
    E p ∩ G ∩ ↑(π“˜ p') βŠ† Eβ‚‚ (2 ^ (N + 3)) p'

    We prove inclusion 6.3.24 for every p ∈ (𝔄_aux 𝔄 Ο‘ N) with 𝔰 p' < 𝔰 p such that (π“˜ p : Set X) ∩ (π“˜ p') β‰  βˆ…. The variable p' corresponds to 𝔭_Ο‘ in the blueprint.

    source
    theorem Antichain.local_antichain_density {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) 𝔄) (Ο‘ : Θ X) (N : β„•) {p' : 𝔓 X} (hp' : Ο‘ ∈ ball_{𝔠 p', ↑(defaultD a) ^ 𝔰 p' / 4} (𝒬 p') (2 ^ (N + 1))) :
    βˆ‘ p ∈ (𝔄_aux 𝔄 Ο‘ N).toFinset with 𝔰 p' < 𝔰 p, MeasureTheory.volume (E p ∩ G ∩ ↑(π“˜ p')) ≀ MeasureTheory.volume (Eβ‚‚ (2 ^ (N + 3)) p')

    Lemma 6.3.3.

    source
    def Antichain.C6_3_4 (a N : β„•) :
    NNReal

    The constant appearing in Lemma 6.3.4.

    Equations
    Instances For
      source
      def Antichain.C6_3_4' (a N : β„•) :
      NNReal

      Auxiliary constant for Lemma 6.3.4.

      Equations
      Instances For
        source
        def 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)) (Ο‘ : ↑(Set.range ⇑Q)) (N : β„•) :
        Set (𝔓 X)

        The set 𝔄' defined in Lemma 6.3.4.

        Equations
        Instances For
          source
          def Antichain.𝔄_min {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)) (Ο‘ : ↑(Set.range ⇑Q)) (N : β„•) :
          Set (𝔓 X)

          The set 𝔄_-S defined in Lemma 6.3.4.

          Equations
          Instances For
            source
            def Antichain.𝓛_min {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)) (Ο‘ : ↑(Set.range ⇑Q)) (N : β„•) :
            Set (Grid X)

            The set 𝓛_{-S} defined in Lemma 6.3.4.

            Equations
            Instances For
              source
              def 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)) (Ο‘ : ↑(Set.range ⇑Q)) (N : β„•) :
              Set (Grid X)

              The set 𝓛 defined in Lemma 6.3.4.

              Equations
              Instances For
                source
                theorem Antichain.I_p_subset_union_L {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)) (Ο‘ : ↑(Set.range ⇑Q)) (N : β„•) (p : ↑(𝔄' 𝔄 Ο‘ N)) :
                ↑(π“˜ ↑p) βŠ† ⋃ L ∈ 𝓛 𝔄 Ο‘ N, ↑L
                source
                theorem Antichain.union_L_eq_union_I_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)) (Ο‘ : ↑(Set.range ⇑Q)) (N : β„•) :
                ⋃ L ∈ 𝓛 𝔄 Ο‘ N, ↑L = ⋃ p ∈ 𝔄' 𝔄 Ο‘ N, ↑(π“˜ p)
                source
                def 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)) (Ο‘ : ↑(Set.range ⇑Q)) (N : β„•) :
                Set (Grid X)

                The set 𝓛* defined in Lemma 6.3.4.

                Equations
                Instances For
                  source
                  theorem Antichain.pairwiseDisjoint_𝓛' {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)) (Ο‘ : ↑(Set.range ⇑Q)) (N : β„•) :
                  (↑(𝓛' 𝔄 Ο‘ N).toFinset).PairwiseDisjoint fun (I : Grid X) => ↑I
                  source
                  theorem Antichain.union_L'_eq_union_I_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)) (Ο‘ : ↑(Set.range ⇑Q)) (N : β„•) :
                  ⋃ L ∈ 𝓛' 𝔄 Ο‘ N, ↑L = ⋃ p ∈ 𝔄' 𝔄 Ο‘ N, ↑(π“˜ p)
                  source
                  theorem Antichain.exists_larger_grid {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)} {Ο‘ : ↑(Set.range ⇑Q)} {N : β„•} {L : Grid X} (hL : L ∈ 𝓛' 𝔄 Ο‘ N) :
                  βˆƒ (L' : Grid X), L ≀ L' ∧ s L' = s L + 1
                  source
                  def Antichain.L' {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)} {Ο‘ : ↑(Set.range ⇑Q)} {N : β„•} {L : Grid X} (hL : L ∈ 𝓛' 𝔄 Ο‘ N) :
                  Grid X

                  The L' introduced in the proof of Lemma 6.3.4.

                  Equations
                  Instances For
                    source
                    theorem Antichain.L_le_L' {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)} {Ο‘ : ↑(Set.range ⇑Q)} {N : β„•} {L : Grid X} (hL : L ∈ 𝓛' 𝔄 Ο‘ N) :
                    L ≀ L' hL
                    source
                    theorem Antichain.s_L'_eq {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)} {Ο‘ : ↑(Set.range ⇑Q)} {N : β„•} {L : Grid X} (hL : L ∈ 𝓛' 𝔄 Ο‘ N) :
                    s (L' hL) = s L + 1
                    source
                    theorem Antichain.c_L_mem {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)} {Ο‘ : ↑(Set.range ⇑Q)} {N : β„•} {L : Grid X} (hL : L ∈ 𝓛' 𝔄 Ο‘ N) :
                    c L ∈ L' hL
                    source
                    def Antichain.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)} {Ο‘ : ↑(Set.range ⇑Q)} {N : β„•} {L : Grid X} (hL : L ∈ 𝓛' 𝔄 Ο‘ N) :
                    𝔓 X

                    p'' in the blueprint

                    Equations
                    Instances For
                      source
                      theorem Antichain.p''_mem {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)} {Ο‘ : ↑(Set.range ⇑Q)} {N : β„•} {L : Grid X} (hL : L ∈ 𝓛' 𝔄 Ο‘ N) :
                      p'' hL ∈ 𝔄' 𝔄 Ο‘ N
                      source
                      theorem Antichain.I_p''_le_L' {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)} {Ο‘ : ↑(Set.range ⇑Q)} {N : β„•} {L : Grid X} (hL : L ∈ 𝓛' 𝔄 Ο‘ N) :
                      π“˜ (p'' hL) ≀ L' hL
                      source
                      def Antichain.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)} {Ο‘ : ↑(Set.range ⇑Q)} {N : β„•} {L : Grid X} (hL : L ∈ 𝓛' 𝔄 Ο‘ N) :
                      𝔓 X

                      p_Θ in the blueprint

                      Equations
                      Instances For
                        source
                        theorem Antichain.I_pΘ_eq_L' {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)} {Ο‘ : ↑(Set.range ⇑Q)} {N : β„•} {L : Grid X} (hL : L ∈ 𝓛' 𝔄 Ο‘ N) :
                        π“˜ (pΘ hL) = L' hL
                        source
                        theorem Antichain.theta_mem_Omega_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)} {Ο‘ : ↑(Set.range ⇑Q)} {N : β„•} {L : Grid X} (hL : L ∈ 𝓛' 𝔄 Ο‘ N) (h : Β¬π“˜ (p'' hL) = L' hL) :
                        ↑ϑ ∈ Ξ© (pΘ hL)
                        source
                        theorem Antichain.pΘ_unique {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)} {Ο‘ : ↑(Set.range ⇑Q)} {N : β„•} {L : Grid X} (hL : L ∈ 𝓛' 𝔄 Ο‘ N) (h : Β¬π“˜ (p'' hL) = L' hL) (y : 𝔓 X) :
                        (fun (p : 𝔓 X) => π“˜ p = L' hL ∧ ↑ϑ ∈ Ξ© p) y β†’ y = pΘ hL
                        source
                        theorem Antichain.global_antichain_density_aux {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)} {Ο‘ : ↑(Set.range ⇑Q)} {N : β„•} {L : Grid X} (hL : L ∈ 𝓛' 𝔄 Ο‘ N) (h𝔄 : IsAntichain (fun (x1 x2 : 𝔓 X) => x1 ≀ x2) 𝔄) :
                        βˆ‘ p ∈ (𝔄' 𝔄 Ο‘ N).toFinset, MeasureTheory.volume (E p ∩ G ∩ ↑L) ≀ ↑(C6_3_4' a N) * dens₁ 𝔄 * MeasureTheory.volume ↑L
                        source
                        theorem Antichain.global_antichain_density {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) 𝔄) (Ο‘ : ↑(Set.range ⇑Q)) (N : β„•) :
                        βˆ‘ p ∈ (𝔄_aux 𝔄 (↑ϑ) N).toFinset, MeasureTheory.volume (E p ∩ G) ≀ ↑(C6_3_4 a N) * dens₁ 𝔄 * MeasureTheory.volume (⋃ p ∈ 𝔄, ↑(π“˜ p))

                        Lemma 6.3.4.

                        source
                        def Antichain.p₆ (a : β„•) :
                        ℝ

                        p in Lemma 6.1.6. We append a subscript ₆ to keep p available for tiles.

                        Equations
                        Instances For
                          source
                          def Antichain.q₆ (a : β„•) :
                          ℝ

                          p' in the proof of Lemma 6.1.4, the HΓΆlder conjugate exponent of p₆.

                          Equations
                          Instances For
                            source
                            theorem Antichain.p₆_ge_1024 {a : β„•} (a4 : 4 ≀ a) :
                            1024 ≀ p₆ a
                            source
                            theorem Antichain.one_lt_p₆ {a : β„•} (a4 : 4 ≀ a) :
                            1 < p₆ a
                            source
                            theorem Antichain.p₆_pos {a : β„•} (a4 : 4 ≀ a) :
                            0 < p₆ a
                            source
                            theorem Antichain.holderConjugate_p₆ {a : β„•} (a4 : 4 ≀ a) :
                            (p₆ a).HolderConjugate (q₆ a)
                            source
                            theorem Antichain.q₆_le_superparticular {a : β„•} (a4 : 4 ≀ a) :
                            q₆ a ≀ 1024 / 1023
                            source
                            theorem Antichain.one_lt_q₆ {a : β„•} (a4 : 4 ≀ a) :
                            1 < q₆ a
                            source
                            theorem Antichain.q₆_pos {a : β„•} (a4 : 4 ≀ a) :
                            0 < q₆ a
                            source
                            theorem Antichain.C2_0_6_q₆_le {a : β„•} (a4 : 4 ≀ a) :
                            C2_0_6 (↑(defaultA a)) (q₆ a).toNNReal 2 ≀ 2 ^ (a + 2)

                            A very involved bound needed for Lemma 6.1.4.

                            source
                            theorem Antichain.tile_count_aux {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) 𝔄) (Ο‘ : ↑(Set.range ⇑Q)) {n : β„•} :
                            MeasureTheory.eLpNorm (fun (x : X) => βˆ‘ p ∈ (𝔄_aux 𝔄 (↑ϑ) n).toFinset, 2 ^ (-↑n * (2 * ↑a ^ 2 + ↑a ^ 3)⁻¹) * (E p).indicator 1 x * G.indicator 1 x) (ENNReal.ofReal (p₆ a)) MeasureTheory.volume ≀ (2 ^ ((↑𝕔 + 1) * ↑a ^ 3 - ↑n)) ^ (p₆ a)⁻¹ * dens₁ 𝔄 ^ (p₆ a)⁻¹ * MeasureTheory.volume (⋃ p ∈ 𝔄, ↑(π“˜ p)) ^ (p₆ a)⁻¹
                            source
                            def Antichain.C6_1_6 (a : β„•) :
                            NNReal

                            The constant appearing in Lemma 6.1.6.

                            Equations
                            Instances For
                              source
                              theorem Antichain.le_C6_1_6 {a : β„•} (N : β„•) (a4 : 4 ≀ a) :
                              2 ^ ((↑𝕔 + 1) * ↑a ^ 3 / p₆ a) * βˆ‘ n ∈ Finset.range N, (2 ^ (-(p₆ a)⁻¹)) ^ n ≀ ↑(C6_1_6 a)
                              source
                              theorem Antichain.tile_count {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) 𝔄) (Ο‘ : ↑(Set.range ⇑Q)) :
                              MeasureTheory.eLpNorm (fun (x : X) => βˆ‘ p : 𝔓 X with p ∈ 𝔄, (1 + edist_{𝔠 p, ↑(defaultD a) ^ 𝔰 p / 4} (𝒬 p) ↑ϑ) ^ (-(2 * ↑a ^ 2 + ↑a ^ 3)⁻¹) * (E p).indicator 1 x * G.indicator 1 x) (ENNReal.ofReal (p₆ a)) MeasureTheory.volume ≀ ↑(C6_1_6 a) * dens₁ 𝔄 ^ (p₆ a)⁻¹ * MeasureTheory.volume (⋃ p ∈ 𝔄, ↑(π“˜ p)) ^ (p₆ a)⁻¹

                              Lemma 6.1.6.