Documentation

Carleson.TileStructure

source
class PreTileStructure {π•œ : Type u_1} [RCLike π•œ] {X : Type u} {A : outParam NNReal} [PseudoMetricSpace X] [MeasureTheory.DoublingMeasure X A] [FunctionDistances π•œ X] (Q : outParam (MeasureTheory.SimpleFunc X (Θ X))) (D : outParam β„•) (ΞΊ : outParam ℝ) (S : outParam β„•) (o : outParam X) extends GridStructure X D ΞΊ S o :
Type (max (u + 1) (u_2 + 1))
Instances
    source
    def 𝔓 {π•œ : Type u_1} [RCLike π•œ] (X : Type u) {A : NNReal} [PseudoMetricSpace X] [MeasureTheory.DoublingMeasure X A] {D : β„•} {ΞΊ : ℝ} {S : β„•} {o : X} [FunctionDistances π•œ X] {Q : MeasureTheory.SimpleFunc X (Θ X)} [PreTileStructure Q D ΞΊ S o] :
    Type u
    Equations
    Instances For
      source
      instance instFintype𝔓 {π•œ : Type u_1} [RCLike π•œ] {X : Type u} {A : NNReal} [PseudoMetricSpace X] [MeasureTheory.DoublingMeasure X A] {D : β„•} {ΞΊ : ℝ} {S : β„•} {o : X} [FunctionDistances π•œ X] {Q : MeasureTheory.SimpleFunc X (Θ X)} [PreTileStructure Q D ΞΊ S o] :
      Fintype (𝔓 X)
      Equations
      source
      def π“˜ {π•œ : Type u_1} [RCLike π•œ] {X : Type u} {A : NNReal} [PseudoMetricSpace X] [MeasureTheory.DoublingMeasure X A] {D : β„•} {ΞΊ : ℝ} {S : β„•} {o : X} [FunctionDistances π•œ X] {Q : MeasureTheory.SimpleFunc X (Θ X)} [PreTileStructure Q D ΞΊ S o] :
      𝔓 X β†’ Grid X
      Equations
      Instances For
        source
        theorem surjective_π“˜ {π•œ : Type u_1} [RCLike π•œ] {X : Type u} {A : NNReal} [PseudoMetricSpace X] [MeasureTheory.DoublingMeasure X A] {D : β„•} {ΞΊ : ℝ} {S : β„•} {o : X} [FunctionDistances π•œ X] {Q : MeasureTheory.SimpleFunc X (Θ X)} [PreTileStructure Q D ΞΊ S o] :
        Function.Surjective π“˜
        source
        instance instInhabited𝔓 {π•œ : Type u_1} [RCLike π•œ] {X : Type u} {A : NNReal} [PseudoMetricSpace X] [MeasureTheory.DoublingMeasure X A] {D : β„•} {ΞΊ : ℝ} {S : β„•} {o : X} [FunctionDistances π•œ X] {Q : MeasureTheory.SimpleFunc X (Θ X)} [PreTileStructure Q D ΞΊ S o] :
        Inhabited (𝔓 X)
        Equations
        source
        def 𝔠 {π•œ : Type u_1} [RCLike π•œ] {X : Type u} {A : NNReal} [PseudoMetricSpace X] [MeasureTheory.DoublingMeasure X A] {D : β„•} {ΞΊ : ℝ} {S : β„•} {o : X} [FunctionDistances π•œ X] {Q : MeasureTheory.SimpleFunc X (Θ X)} [PreTileStructure Q D ΞΊ S o] (p : 𝔓 X) :
        X
        Equations
        Instances For
          source
          def 𝔰 {π•œ : Type u_1} [RCLike π•œ] {X : Type u} {A : NNReal} [PseudoMetricSpace X] [MeasureTheory.DoublingMeasure X A] {D : β„•} {ΞΊ : ℝ} {S : β„•} {o : X} [FunctionDistances π•œ X] {Q : MeasureTheory.SimpleFunc X (Θ X)} [PreTileStructure Q D ΞΊ S o] (p : 𝔓 X) :
          β„€
          Equations
          Instances For
            source
            class TileStructure {X : Type u} {A : outParam NNReal} [PseudoMetricSpace X] [MeasureTheory.DoublingMeasure X A] [FunctionDistances ℝ X] (Q : outParam (MeasureTheory.SimpleFunc X (Θ X))) (D : outParam β„•) (ΞΊ : outParam ℝ) (S : outParam β„•) (o : outParam X) extends PreTileStructure Q D ΞΊ S o :
            Type (u + 1)

            A tile structure.

            Instances
              source
              def Β«termDist_(_)Β» :
              Lean.ParserDescr
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                def Β«termNndist_(_)Β» :
                Lean.ParserDescr
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  def Β«termBall_(_)Β» :
                  Lean.ParserDescr
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    @[simp]
                    theorem dist_π“˜ {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {f g : Θ X} (p : 𝔓 X) :
                    dist f g = dist f g
                    source
                    @[simp]
                    theorem nndist_π“˜ {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {f g : Θ X} (p : 𝔓 X) :
                    nndist f g = nndist f g
                    source
                    @[simp]
                    theorem ball_π“˜ {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {f : Θ X} (p : 𝔓 X) {r : ℝ} :
                    Metric.ball f r = Metric.ball f r
                    source
                    @[simp]
                    theorem cball_subset {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {p : 𝔓 X} :
                    Metric.ball (𝒬 p) 5⁻¹ βŠ† Ξ© p
                    source
                    @[simp]
                    theorem subset_cball {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {p : 𝔓 X} :
                    Ξ© p βŠ† Metric.ball (𝒬 p) 1
                    source
                    theorem ball_eq_of_grid_eq {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {p q✝ : 𝔓 X} {Ο‘ : Θ X} {r : ℝ} (h : π“˜ p = π“˜ q✝) :
                    Metric.ball Ο‘ r = Metric.ball Ο‘ r
                    source
                    theorem cball_disjoint {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {p p' : 𝔓 X} (h : p β‰  p') (hp : π“˜ p = π“˜ p') :
                    Disjoint (Metric.ball (𝒬 p) 5⁻¹) (Metric.ball (𝒬 p') 5⁻¹)
                    source
                    def E {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] (p : 𝔓 X) :
                    Set X

                    The set E defined in Proposition 2.0.2.

                    Equations
                    Instances For
                      source
                      theorem E_subset_π“˜ {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {p : 𝔓 X} :
                      E p βŠ† ↑(π“˜ p)
                      source
                      theorem measurableSet_E {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {p : 𝔓 X} :
                      MeasurableSet (E p)
                      source
                      theorem volume_E_lt_top {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {p : 𝔓 X} :
                      MeasureTheory.volume (E p) < ⊀
                      source
                      def carlesonOn {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] (p : 𝔓 X) (f : X β†’ β„‚) :
                      X β†’ β„‚

                      The operator T_𝔭 defined in Proposition 2.0.2, considered on the set F. It is the map T ∘ (1_F * Β·) : f ↦ T (1_F * f), also denoted T1_F The operator T in Proposition 2.0.2 is therefore applied to (F := Set.univ).

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        source
                        theorem measurable_carlesonOn {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {p : 𝔓 X} {f : X β†’ β„‚} (measf : Measurable f) :
                        Measurable (carlesonOn p f)
                        source
                        def carlesonSum {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] (β„­ : Set (𝔓 X)) (f : X β†’ β„‚) (x : X) :
                        β„‚

                        The operator T_β„­ f defined at the bottom of Section 7.4. We will use this in other places of the formalization as well.

                        Equations
                        Instances For
                          source
                          theorem measurable_carlesonSum {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {β„­ : Set (𝔓 X)} {f : X β†’ β„‚} (measf : Measurable f) :
                          Measurable (carlesonSum β„­ f)
                          source
                          theorem MeasureTheory.AEStronglyMeasurable.carlesonOn {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {p : 𝔓 X} {f : X β†’ β„‚} (hf : AEStronglyMeasurable f volume) :
                          AEStronglyMeasurable (_root_.carlesonOn p f) volume
                          source
                          theorem MeasureTheory.AEStronglyMeasurable.carlesonSum {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {β„­ : Set (𝔓 X)} {f : X β†’ β„‚} (hf : AEStronglyMeasurable f volume) :
                          AEStronglyMeasurable (_root_.carlesonSum β„­ f) volume
                          source
                          theorem carlesonOn_def' {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] (p : 𝔓 X) (f : X β†’ β„‚) :
                          carlesonOn p f = (E p).indicator fun (x : X) => ∫ (y : X), Ks (𝔰 p) x y * f y * Complex.exp (Complex.I * (↑((Q x) y) - ↑((Q x) x)))
                          source
                          theorem support_carlesonOn_subset_E {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {p : 𝔓 X} {f : X β†’ β„‚} :
                          Function.support (carlesonOn p f) βŠ† E p
                          source
                          theorem support_carlesonSum_subset {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {β„­ : Set (𝔓 X)} {f : X β†’ β„‚} :
                          Function.support (carlesonSum β„­ f) βŠ† ⋃ p ∈ β„­, ↑(π“˜ p)
                          source
                          theorem MeasureTheory.BoundedCompactSupport.carlesonOn {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {p : 𝔓 X} {f : X β†’ β„‚} (hf : BoundedCompactSupport f) :
                          BoundedCompactSupport (_root_.carlesonOn p f)
                          source
                          theorem MeasureTheory.BoundedCompactSupport.carlesonSum {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {β„­ : Set (𝔓 X)} {f : X β†’ β„‚} (hf : BoundedCompactSupport f) :
                          BoundedCompactSupport (_root_.carlesonSum β„­ f)
                          source
                          theorem carlesonSum_inter_add_inter_compl {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {f : X β†’ β„‚} {x : X} (A B : Set (𝔓 X)) :
                          carlesonSum (A ∩ B) f x + carlesonSum (A ∩ Bᢜ) f x = carlesonSum A f x
                          source
                          theorem sum_carlesonSum_of_pairwiseDisjoint {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {ΞΉ : Type u_2} {f : X β†’ β„‚} {x : X} {A : ΞΉ β†’ Set (𝔓 X)} {s : Finset ΞΉ} (hs : (↑s).PairwiseDisjoint A) :
                          βˆ‘ i ∈ s, carlesonSum (A i) f x = carlesonSum (⋃ i ∈ s, A i) f x
                          source
                          def TileLike (X : Type u_1) [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] :
                          Type u_1
                          Equations
                          Instances For
                            source
                            def TileLike.fst {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] (x : TileLike X) :
                            Grid X
                            Equations
                            • x.fst = x.1
                            Instances For
                              source
                              def TileLike.snd {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] (x : TileLike X) :
                              Set (Θ X)
                              Equations
                              • x.snd = x.2
                              Instances For
                                source
                                @[simp]
                                theorem TileLike.fst_mk {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] (x : Grid X) (y : Set (Θ X)) :
                                fst (x, y) = x
                                source
                                @[simp]
                                theorem TileLike.snd_mk {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] (x : Grid X) (y : Set (Θ X)) :
                                snd (x, y) = y
                                source
                                instance instPartialOrderTileLike {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] :
                                PartialOrder (TileLike X)
                                Equations
                                source
                                theorem TileLike.le_def {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] (x y : TileLike X) :
                                x ≀ y ↔ x.fst ≀ y.fst ∧ y.snd βŠ† x.snd
                                source
                                def toTileLike {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] (p : 𝔓 X) :
                                TileLike X
                                Equations
                                Instances For
                                  source
                                  @[simp]
                                  theorem toTileLike_fst {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] (p : 𝔓 X) :
                                  (toTileLike p).fst = π“˜ p
                                  source
                                  @[simp]
                                  theorem toTileLike_snd {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] (p : 𝔓 X) :
                                  (toTileLike p).snd = Ξ© p
                                  source
                                  def smul {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] (l : ℝ) (p : 𝔓 X) :
                                  TileLike X

                                  This is not defined as such in the blueprint, but Ξ»p ≲ Ξ»'p' can be written using smul l p ≀ smul l' p'. Beware: smul 1 p is very different from toTileLike p.

                                  Equations
                                  Instances For
                                    source
                                    @[simp]
                                    theorem smul_fst {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] (l : ℝ) (p : 𝔓 X) :
                                    (smul l p).fst = π“˜ p
                                    source
                                    @[simp]
                                    theorem smul_snd {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] (l : ℝ) (p : 𝔓 X) :
                                    (smul l p).snd = Metric.ball (𝒬 p) l
                                    source
                                    theorem smul_mono_left {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {l l' : ℝ} {p : 𝔓 X} (h : l ≀ l') :
                                    smul l' p ≀ smul l p
                                    source
                                    theorem smul_le_toTileLike {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {p : 𝔓 X} :
                                    smul 1 p ≀ toTileLike p
                                    source
                                    theorem toTileLike_le_smul {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {p : 𝔓 X} :
                                    toTileLike p ≀ smul 5⁻¹ p
                                    source
                                    theorem 𝒬_mem_Ξ© {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {p : 𝔓 X} :
                                    𝒬 p ∈ Ξ© p
                                    source
                                    theorem 𝒬_inj {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {p p' : 𝔓 X} (h : 𝒬 p = 𝒬 p') (hπ“˜ : π“˜ p = π“˜ p') :
                                    p = p'
                                    source
                                    theorem toTileLike_injective {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] :
                                    Function.Injective fun (p : 𝔓 X) => toTileLike p
                                    source
                                    instance instPartialOrder𝔓Real {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] :
                                    PartialOrder (𝔓 X)
                                    Equations
                                    source
                                    theorem 𝔓.le_def {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {p q✝ : 𝔓 X} :
                                    p ≀ q✝ ↔ toTileLike p ≀ toTileLike q✝
                                    source
                                    theorem 𝔓.le_def' {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {p q✝ : 𝔓 X} :
                                    p ≀ q✝ ↔ π“˜ p ≀ π“˜ q✝ ∧ Ξ© q✝ βŠ† Ξ© p
                                    source
                                    theorem dist_𝒬_lt_one_of_le {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {p q✝ : 𝔓 X} (h : p ≀ q✝) :
                                    dist (𝒬 q✝) (𝒬 p) < 1
                                    source
                                    theorem dist_𝒬_lt_one_of_le' {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {p q✝ : 𝔓 X} (h : p ≀ q✝) :
                                    dist (𝒬 p) (𝒬 q✝) < 1
                                    source
                                    theorem π“˜_strictMono {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] :
                                    StrictMono π“˜
                                    source
                                    theorem smul_mono {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {p p' : 𝔓 X} {m m' n n' : ℝ} (hp : smul n p ≀ smul m p') (hm : m' ≀ m) (hn : n ≀ n') :
                                    smul n' p ≀ smul m' p'

                                    Lemma 5.3.1

                                    source
                                    theorem smul_C2_1_2 {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {p p' : 𝔓 X} (m : ℝ) {n k : ℝ} (hk : 0 < k) (hp : π“˜ p β‰  π“˜ p') (hl : smul n p ≀ smul k p') :
                                    smul (n + C2_1_2 a * m) p ≀ smul m p'

                                    Lemma 5.3.2 (generalizing 1 to k > 0)

                                    source
                                    theorem dist_LTSeries {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} {u : Set (𝔓 X)} {s : LTSeries ↑u} (hs : s.length = n) {f g : Θ X} :
                                    dist f g ≀ C2_1_2 a ^ n * dist f g
                                    source
                                    def C5_3_3 (a : β„•) :
                                    ℝ

                                    The constraint on Ξ» in the first part of Lemma 5.3.3.

                                    Equations
                                    Instances For
                                      source
                                      theorem C5_3_3_le {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] :
                                      C5_3_3 a ≀ 11 / 10
                                      source
                                      theorem wiggle_order_11_10 {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {p p' : 𝔓 X} {n : ℝ} (hp : p ≀ p') (hn : C5_3_3 a ≀ n) :
                                      smul n p ≀ smul n p'

                                      Lemma 5.3.3, Equation (5.3.3)

                                      source
                                      theorem wiggle_order_100 {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {p p' : 𝔓 X} (hp : smul 10 p ≀ smul 1 p') (hn : π“˜ p β‰  π“˜ p') :
                                      smul 100 p ≀ smul 100 p'

                                      Lemma 5.3.3, Equation (5.3.4)

                                      source
                                      theorem wiggle_order_500 {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {p p' : 𝔓 X} (hp : smul 2 p ≀ smul 1 p') (hn : π“˜ p β‰  π“˜ p') :
                                      smul 4 p ≀ smul 500 p'

                                      Lemma 5.3.3, Equation (5.3.5)

                                      source
                                      def C5_3_2 (a : β„•) :
                                      ℝ
                                      Equations
                                      Instances For
                                        source
                                        def TileLike.toTile {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] (t : TileLike X) :
                                        Set (X Γ— Θ X)
                                        Equations
                                        Instances For
                                          source
                                          def TileLike.toSet {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] (t : TileLike X) :
                                          Set X

                                          From a TileLike, we can construct a set. This is used in the definitions E₁ and Eβ‚‚.

                                          Equations
                                          Instances For
                                            source
                                            def E₁ {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] (p : 𝔓 X) :
                                            Set X
                                            Equations
                                            Instances For
                                              source
                                              def Eβ‚‚ {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] (l : ℝ) (p : 𝔓 X) :
                                              Set X
                                              Equations
                                              Instances For
                                                source
                                                theorem E₁_subset {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] (p : 𝔓 X) :
                                                E₁ p βŠ† ↑(π“˜ p)
                                                source
                                                theorem Eβ‚‚_subset {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] (l : ℝ) (p : 𝔓 X) :
                                                Eβ‚‚ l p βŠ† ↑(π“˜ p)

                                                𝔓(𝔓') in the blueprint is lowerClosure 𝔓' in Lean.

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

                                                This density is defined to live in ℝβ‰₯0∞. Use ENNReal.toReal to get a real number.

                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                Instances For
                                                  source
                                                  theorem dens₁_mono {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {𝔓₁ 𝔓₂ : Set (𝔓 X)} (h : 𝔓₁ βŠ† 𝔓₂) :
                                                  dens₁ 𝔓₁ ≀ dens₁ 𝔓₂
                                                  source
                                                  def densβ‚‚ {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] (𝔓' : Set (𝔓 X)) :
                                                  ENNReal

                                                  This density is defined to live in ℝβ‰₯0∞. Use ENNReal.toReal to get a real number.

                                                  Equations
                                                  Instances For
                                                    source
                                                    theorem densβ‚‚_eq_biSup_densβ‚‚ {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] (𝔓' : Set (𝔓 X)) :
                                                    densβ‚‚ 𝔓' = ⨆ p ∈ 𝔓', densβ‚‚ {p}
                                                    source
                                                    theorem isAntichain_iff_disjoint {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] (𝔄 : Set (𝔓 X)) :
                                                    IsAntichain (fun (x1 x2 : TileLike X) => x1 ≀ x2) (toTileLike '' 𝔄) ↔ βˆ€ (p p' : 𝔓 X), p ∈ 𝔄 β†’ p' ∈ 𝔄 β†’ p β‰  p' β†’ Disjoint (toTileLike p).toTile (toTileLike p').toTile
                                                    source
                                                    theorem ENNReal.rpow_le_rpow_of_nonpos {x y : ENNReal} {z : ℝ} (hz : z ≀ 0) (h : x ≀ y) :
                                                    y ^ z ≀ x ^ z
                                                    source
                                                    def dens₁_le_one {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {𝔓' : Set (𝔓 X)} :
                                                    dens₁ 𝔓' ≀ 1
                                                    Equations
                                                    • β‹― = β‹―
                                                    Instances For

                                                      Stack sizes #

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

                                                      The number of tiles p in s whose underlying cube π“˜ p contains x.

                                                      Equations
                                                      Instances For
                                                        source
                                                        theorem stackSize_setOf_add_stackSize_setOf_not {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {C : Set (𝔓 X)} {x : X} {P : 𝔓 X β†’ Prop} :
                                                        stackSize {p : 𝔓 X | p ∈ C ∧ P p} x + stackSize {p : 𝔓 X | p ∈ C ∧ Β¬P p} x = stackSize C x
                                                        source
                                                        theorem stackSize_congr {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {C : Set (𝔓 X)} {x x' : X} (h : βˆ€ p ∈ C, x ∈ ↑(π“˜ p) ↔ x' ∈ ↑(π“˜ p)) :
                                                        stackSize C x = stackSize C x'
                                                        source
                                                        theorem stackSize_mono {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {C C' : Set (𝔓 X)} {x : X} (h : C βŠ† C') :
                                                        stackSize C x ≀ stackSize C' x
                                                        source
                                                        theorem stackSize_real {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] (C : Set (𝔓 X)) (x : X) :
                                                        ↑(stackSize C x) = βˆ‘ p ∈ Finset.filter (fun (p : 𝔓 X) => p ∈ C) Finset.univ, (↑(π“˜ p)).indicator 1 x
                                                        source
                                                        theorem stackSize_measurable {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {C : Set (𝔓 X)} :
                                                        Measurable fun (x : X) => ↑(stackSize C x)
                                                        source
                                                        theorem stackSize_le_one_of_pairwiseDisjoint {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {C : Set (𝔓 X)} {x : X} (h : C.PairwiseDisjoint fun (p : 𝔓 X) => ↑(π“˜ p)) :
                                                        stackSize C x ≀ 1

                                                        Decomposing a set of tiles into disjoint subfamilies #

                                                        source
                                                        theorem exists_maximal_disjoint_covering_subfamily {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] (A : Set (𝔓 X)) :
                                                        βˆƒ (B : Set (𝔓 X)), (B.PairwiseDisjoint fun (p : 𝔓 X) => ↑(π“˜ p)) ∧ B βŠ† A ∧ βˆ€ a_1 ∈ A, βˆƒ b ∈ B, ↑(π“˜ a_1) βŠ† ↑(π“˜ b)

                                                        Given any family of tiles, one can extract a maximal disjoint subfamily, covering everything.

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

                                                        A disjoint subfamily of A covering everything.

                                                        Equations
                                                        Instances For
                                                          source
                                                          @[irreducible]
                                                          def iteratedMaximalSubfamily {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] (A : Set (𝔓 X)) (n : β„•) :
                                                          Set (𝔓 X)

                                                          Iterating maximalSubfamily to obtain disjoint subfamilies of A.

                                                          Equations
                                                          Instances For
                                                            source
                                                            theorem pairwiseDisjoint_iteratedMaximalSubfamily_image {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] (A : Set (𝔓 X)) (n : β„•) :
                                                            (iteratedMaximalSubfamily A n).PairwiseDisjoint fun (p : 𝔓 X) => ↑(π“˜ p)
                                                            source
                                                            theorem iteratedMaximalSubfamily_subset {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] (A : Set (𝔓 X)) (n : β„•) :
                                                            iteratedMaximalSubfamily A n βŠ† A
                                                            source
                                                            theorem pairwiseDisjoint_iteratedMaximalSubfamily {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] (A : Set (𝔓 X)) :
                                                            Set.univ.PairwiseDisjoint (iteratedMaximalSubfamily A)
                                                            source
                                                            theorem eq_biUnion_iteratedMaximalSubfamily {X : Type u_1} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] (A : Set (𝔓 X)) {N : β„•} (hN : βˆ€ (x : X), stackSize A x ≀ N) :
                                                            A = ⋃ (n : β„•), ⋃ (_ : n < N), iteratedMaximalSubfamily A n

                                                            Any set of tiles can be written as the union of disjoint subfamilies, their number being controlled by the maximal stack size.