Documentation

Carleson.Forest

source
structure TileStructure.Forest (X : Type u_1) [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] (n : β„•) :
Type u_1

An n-forest

Instances For
    source
    theorem TileStructure.Forest.nonempty' {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} (self : TileStructure.Forest X n) {u : 𝔓 X} (hu : u ∈ self.π”˜) :
    (self.𝔗 u).Nonempty
    source
    theorem TileStructure.Forest.ordConnected' {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} (self : TileStructure.Forest X n) {u : 𝔓 X} (hu : u ∈ self.π”˜) :
    (self.𝔗 u).OrdConnected
    source
    theorem TileStructure.Forest.π“˜_ne_π“˜' {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} (self : TileStructure.Forest X n) {u : 𝔓 X} (hu : u ∈ self.π”˜) {p : 𝔓 X} (hp : p ∈ self.𝔗 u) :
    π“˜ p β‰  π“˜ u
    source
    theorem TileStructure.Forest.smul_four_le' {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} (self : TileStructure.Forest X n) {u : 𝔓 X} (hu : u ∈ self.π”˜) {p : 𝔓 X} (hp : p ∈ self.𝔗 u) :
    smul 4 p ≀ smul 1 u
    source
    theorem TileStructure.Forest.stackSize_le' {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} (self : TileStructure.Forest X n) {x : X} :
    stackSize self.π”˜ x ≀ 2 ^ n
    source
    theorem TileStructure.Forest.dens₁_𝔗_le' {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} (self : TileStructure.Forest X n) {u : 𝔓 X} (hu : u ∈ self.π”˜) :
    dens₁ (self.𝔗 u) ≀ 2 ^ (4 * ↑a - ↑n + 1)
    source
    theorem TileStructure.Forest.lt_dist' {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} (self : TileStructure.Forest X n) {u : 𝔓 X} {u' : 𝔓 X} (hu : u ∈ self.π”˜) (hu' : u' ∈ self.π”˜) (huu' : u β‰  u') {p : 𝔓 X} (hp : p ∈ self.𝔗 u') (h : π“˜ p ≀ π“˜ u) :
    2 ^ (defaultZ a * (n + 1)) < dist (𝒬 p) (𝒬 u)
    source
    theorem TileStructure.Forest.ball_subset' {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} (self : TileStructure.Forest X n) {u : 𝔓 X} (hu : u ∈ self.π”˜) {p : 𝔓 X} (hp : p ∈ self.𝔗 u) :
    Metric.ball (𝔠 p) (8 * ↑(defaultD a) ^ 𝔰 p) βŠ† ↑(π“˜ u)
    source
    instance TileStructure.Forest.instCoeHeadSet𝔓Real {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} :
    CoeHead (TileStructure.Forest X n) (Set (𝔓 X))
    Equations
    • TileStructure.Forest.instCoeHeadSet𝔓Real = { coe := TileStructure.Forest.π”˜ }
    source
    instance TileStructure.Forest.instMembership𝔓Real {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} :
    Membership (𝔓 X) (TileStructure.Forest X n)
    Equations
    source
    instance TileStructure.Forest.instCoeFunForall𝔓RealSet {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} :
    CoeFun (TileStructure.Forest X n) fun (x : TileStructure.Forest X n) => 𝔓 X β†’ Set (𝔓 X)
    Equations
    source
    @[simp]
    theorem TileStructure.Forest.mem_π”˜ {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {u : 𝔓 X} {n : β„•} (t : TileStructure.Forest X n) :
    u ∈ t.π”˜ ↔ u ∈ t
    source
    @[simp]
    theorem TileStructure.Forest.mem_𝔗 {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {u : 𝔓 X} {p : 𝔓 X} {n : β„•} (t : TileStructure.Forest X n) :
    p ∈ t.𝔗 u ↔ p ∈ (fun (x : 𝔓 X) => t.𝔗 x) u
    source
    theorem TileStructure.Forest.nonempty {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {u : 𝔓 X} {n : β„•} (t : TileStructure.Forest X n) (hu : u ∈ t) :
    ((fun (x : 𝔓 X) => t.𝔗 x) u).Nonempty
    source
    theorem TileStructure.Forest.ordConnected {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {u : 𝔓 X} {n : β„•} (t : TileStructure.Forest X n) (hu : u ∈ t) :
    ((fun (x : 𝔓 X) => t.𝔗 x) u).OrdConnected
    source
    theorem TileStructure.Forest.π“˜_ne_π“˜ {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {u : 𝔓 X} {p : 𝔓 X} {n : β„•} (t : TileStructure.Forest X n) (hu : u ∈ t) (hp : p ∈ (fun (x : 𝔓 X) => t.𝔗 x) u) :
    π“˜ p β‰  π“˜ u
    source
    theorem TileStructure.Forest.smul_four_le {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {u : 𝔓 X} {p : 𝔓 X} {n : β„•} (t : TileStructure.Forest X n) (hu : u ∈ t) (hp : p ∈ (fun (x : 𝔓 X) => t.𝔗 x) u) :
    smul 4 p ≀ smul 1 u
    source
    theorem TileStructure.Forest.stackSize_le {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {x : X} {n : β„•} (t : TileStructure.Forest X n) :
    stackSize t.π”˜ x ≀ 2 ^ n
    source
    theorem TileStructure.Forest.dens₁_𝔗_le {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {u : 𝔓 X} {n : β„•} (t : TileStructure.Forest X n) (hu : u ∈ t) :
    dens₁ ((fun (x : 𝔓 X) => t.𝔗 x) u) ≀ 2 ^ (4 * ↑a - ↑n + 1)
    source
    theorem TileStructure.Forest.lt_dist {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {u : 𝔓 X} {u' : 𝔓 X} {n : β„•} (t : TileStructure.Forest X n) (hu : u ∈ t) (hu' : u' ∈ t) (huu' : u β‰  u') {p : 𝔓 X} (hp : p ∈ (fun (x : 𝔓 X) => t.𝔗 x) u') (h : π“˜ p ≀ π“˜ u) :
    2 ^ (defaultZ a * (n + 1)) < dist (𝒬 p) (𝒬 u)
    source
    theorem TileStructure.Forest.ball_subset {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {u : 𝔓 X} {p : 𝔓 X} {n : β„•} (t : TileStructure.Forest X n) (hu : u ∈ t) (hp : p ∈ (fun (x : 𝔓 X) => t.𝔗 x) u) :
    Metric.ball (𝔠 p) (8 * ↑(defaultD a) ^ 𝔰 p) βŠ† ↑(π“˜ u)
    source
    structure TileStructure.Row (X : Type u_1) [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] (n : β„•) extends TileStructure.Forest :
    Type u_1

    An n-row

    Instances For
      source
      theorem TileStructure.Row.pairwiseDisjoint' {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} (self : TileStructure.Row X n) :
      self.π”˜.PairwiseDisjoint self.𝔗
      source
      instance TileStructure.Row.instCoeHeadSet𝔓Real {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} :
      CoeHead (TileStructure.Row X n) (Set (𝔓 X))
      Equations
      • TileStructure.Row.instCoeHeadSet𝔓Real = { coe := fun (t : TileStructure.Row X n) => t.π”˜ }
      source
      instance TileStructure.Row.instMembership𝔓Real {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} :
      Membership (𝔓 X) (TileStructure.Row X n)
      Equations
      source
      instance TileStructure.Row.instCoeFunForall𝔓RealSet {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} :
      CoeFun (TileStructure.Row X n) fun (x : TileStructure.Row X n) => 𝔓 X β†’ Set (𝔓 X)
      Equations
      source
      @[simp]
      theorem TileStructure.Row.mem_π”˜ {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {u : 𝔓 X} {n : β„•} (t : TileStructure.Row X n) :
      u ∈ t.π”˜ ↔ u ∈ t
      source
      @[simp]
      theorem TileStructure.Row.mem_𝔗 {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {u : 𝔓 X} {p : 𝔓 X} {n : β„•} (t : TileStructure.Row X n) :
      p ∈ t.𝔗 u ↔ p ∈ (fun (x : 𝔓 X) => t.𝔗 x) u
      source
      theorem TileStructure.Row.pairwiseDisjoint {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} (t : TileStructure.Row X n) :
      t.π”˜.PairwiseDisjoint fun (x : 𝔓 X) => t.𝔗 x