Documentation

Carleson.Antichain.AntichainTileCount

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)] (ha : 4 ≀ a) {Ο‘ : Θ X} {N : β„•} {p p' : 𝔓 X} (hp : dist (𝒬 p) Ο‘ ≀ 2 ^ N) (hp' : dist (𝒬 p') Ο‘ ≀ 2 ^ N) (hI : π“˜ p ≀ π“˜ p') (hs : 𝔰 p < 𝔰 p') :
smul (2 ^ (N + 2)) p ≀ smul (2 ^ (N + 2)) p'
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)] (𝔄 : Finset (𝔓 X)) (Ο‘ : Θ X) (N : β„•) :
Finset (𝔓 X)
Equations
Instances For
    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)] (𝔄 : Finset (𝔓 X)) (Ο‘ : Θ X) (N : β„•) (L : Grid X) :
    βˆ‘ p ∈ Finset.filter (fun (p : 𝔓 X) => π“˜ p = L) (Antichain.𝔄_aux 𝔄 Ο‘ N), MeasureTheory.volume (E p ∩ G) ≀ 2 ^ (a * (N + 5)) * dens₁ ↑𝔄 * MeasureTheory.volume ↑L
    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)] (ha : 4 ≀ a) {𝔄 : Finset (𝔓 X)} (Ο‘ : Θ X) (N : β„•) {p p' : 𝔓 X} (hpin : p ∈ Antichain.𝔄_aux 𝔄 Ο‘ N) (hp' : Ο‘ ∈ Ξ© p') (hs : 𝔰 p' < 𝔰 p) (hπ“˜ : (↑(π“˜ p') ∩ ↑(π“˜ p)).Nonempty) :
    E p ∩ G ∩ ↑(π“˜ p') βŠ† Eβ‚‚ (2 ^ (N + 3)) p'
    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)] (ha : 4 ≀ a) {𝔄 : Finset (𝔓 X)} (h𝔄 : IsAntichain (fun (x1 x2 : 𝔓 X) => x1 ≀ x2) ↑𝔄) (Ο‘ : Θ X) (N : β„•) {p' : 𝔓 X} (hp' : Ο‘ ∈ Ξ© p') :
    βˆ‘ p ∈ Finset.filter (fun (p : 𝔓 X) => 𝔰 p' < 𝔰 p) (Antichain.𝔄_aux 𝔄 Ο‘ N), MeasureTheory.volume (E p ∩ G ∩ ↑(π“˜ p')) ≀ MeasureTheory.volume (Eβ‚‚ (2 ^ (N + 3)) p')
    source
    def Antichain.C_6_3_4 (a N : β„•) :
    NNReal
    Equations
    Instances For
      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)] (𝔄 : Finset (𝔓 X)) (Ο‘ : Θ X) (N : β„•) :
      βˆ‘ p ∈ Antichain.𝔄_aux 𝔄 Ο‘ N, MeasureTheory.volume (E p ∩ G) ≀ ↑(Antichain.C_6_3_4 a N) * dens₁ ↑𝔄 * MeasureTheory.volume (⋃ p ∈ 𝔄, ↑(π“˜ p))
      source
      def Antichain.C_6_1_6 (a : β„•) :
      NNReal
      Equations
      Instances For
        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)] {𝔄 𝔄' : Finset (𝔓 X)} (h_le : 𝔄' βŠ† 𝔄) (Ο‘ : Θ X) :
        MeasureTheory.eLpNorm (βˆ‘ 𝔭 ∈ 𝔄', (1 + dist (𝒬 𝔭) Ο‘) ^ (-1 / (2 * ↑a ^ 2 + ↑a ^ 3)) β€’ (E 𝔭).indicator 1 * G.indicator 1) (↑(Antichain.p a)) MeasureTheory.volume ≀ ↑(Antichain.C_6_1_6 a) * dens₁ ↑𝔄 ^ (1 / ↑(Antichain.p a)) * MeasureTheory.volume (⋃ p ∈ 𝔄, ↑(π“˜ p)) ^ (1 / ↑(Antichain.p a))