OAI/Analysis/LipschitzHilbert/Phase/AngularBoundary.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LipschitzHilbert.AngularGrid.index_eq_of_add line 18
2. theorem OAI.LipschitzHilbert.AngularGrid.index_eq_of_le line 28
3. theorem OAI.LipschitzHilbert.AngularGrid.eligible_of_add line 34
4. theorem OAI.LipschitzHilbert.AngularGrid.eligible_of_le line 44
5. theorem OAI.LipschitzHilbert.AngularGrid.cellTops_subset_ancestor line 51

   Source documentation

   Tops in a descendant cell remain eligible and lie in its actual ancestor.

   theorem cellTops_subset_ancestor (g : AngularGrid) (tops : Finset ι)
       (slope precision : ι → ℝ) (cutoff : ℝ) (hp : ∀ i ∈ tops, 0 ≤ precision i)
       {base level : ℕ} (hle : base ≤ level) (s : ℝ) :
       g.cellTops tops slope precision cutoff level (g.index level s) ⊆
         g.cellTops tops slope precision cutoff base (g.index base s) := by
   …

   Mentions: OAI.LipschitzHilbert.AngularGrid

6. def OAI.LipschitzHilbert.AngularGrid.outsideNearTops line 63

   Source documentation

   The extra tops come from nearby next-level cells outside the immediate parent, and all belong to the same block ancestor.

   def outsideNearTops (g : AngularGrid) (tops : Finset ι) (slope precision : ι → ℝ)
       (cutoff : ℝ) (base level : ℕ) (gap s : ℝ) : Finset ι := by
   …

   Mentions: OAI.LipschitzHilbert.AngularGrid

7. def OAI.LipschitzHilbert.AngularGrid.boundaryTops line 71
8. theorem OAI.LipschitzHilbert.AngularGrid.parent_subset_boundary line 77
9. theorem OAI.LipschitzHilbert.AngularGrid.boundary_subset_ancestor line 84
10. theorem OAI.LipschitzHilbert.AngularGrid.neighbor_cell_subset_boundary line 96

    Source documentation

    Each neighboring child within the block ancestor is fully included in this boundary mass. This is the inclusion used by weighted selection.

    theorem neighbor_cell_subset_boundary (g : AngularGrid) (tops : Finset ι)
        (slope precision : ι → ℝ) (cutoff : ℝ) (hp : ∀ i ∈ tops, 0 ≤ precision i)
        {base level : ℕ} (hle : base ≤ level) (gap s t : ℝ)
        (hancestor : g.index base t = g.index base s)
        (hnear : g.neighbors (level + 1) gap (g.index (level + 1) s) (g.index (level + 1) t)) :
        g.cellTops tops slope precision cutoff (level + 1) (g.index (level + 1) t) ⊆
          g.boundaryTops tops slope precision cutoff base level gap s := by
    …

    Mentions: OAI.LipschitzHilbert.AngularGrid

11. def OAI.LipschitzHilbert.AngularGrid.boundaryMass line 118
12. theorem OAI.LipschitzHilbert.AngularGrid.boundary_mass_eq line 123

    Source documentation

    The union defining the boundary has no double counting.

    theorem boundary_mass_eq (g : AngularGrid) (tops : Finset ι)
        (slope precision : ι → ℝ) (cutoff : ℝ) (weight : ι → X → ℝ)
        (base level : ℕ) (gap s : ℝ) (x : X) :
        g.boundaryMass tops slope precision cutoff weight base level gap s x =
          g.mass tops slope precision cutoff weight level (g.index level s) x +
          ∑ i ∈ g.outsideNearTops tops slope precision cutoff base level gap s, weight i x := by
    …

    Mentions: OAI.LipschitzHilbert.AngularGrid

13. theorem OAI.LipschitzHilbert.AngularGrid.boundary_mass_bounds line 137

    Source documentation

    The immediate child, parent, boundary and block ancestor have ordered masses.

    theorem boundary_mass_bounds (g : AngularGrid) (tops : Finset ι)
        (slope precision : ι → ℝ) (cutoff : ℝ) (weight : ι → X → ℝ)
        (hp : ∀ i ∈ tops, 0 ≤ precision i) (hw : ∀ i x, 0 ≤ weight i x)
        {base level : ℕ} (hle : base ≤ level) (gap s : ℝ) (x : X) :
        g.mass tops slope precision cutoff weight (level + 1) (g.index (level + 1) s) x ≤
            g.mass tops slope precision cutoff weight level (g.index level s) x ∧
        g.mass tops slope precision cutoff weight level (g.index level s) x ≤
            g.boundaryMass tops slope precision cutoff weight base level gap s x ∧
        g.boundaryMass tops slope precision cutoff weight base level gap s x ≤
            g.mass tops slope precision cutoff weight base (g.index base s) x := by
    …

    Mentions: OAI.LipschitzHilbert.AngularGrid

14. theorem OAI.LipschitzHilbert.AngularGrid.cellTops_disjoint line 160

    Source documentation

    Distinct angular cells have disjoint eligible top sets.

    theorem cellTops_disjoint (g : AngularGrid) (tops : Finset ι)
        (slope precision : ι → ℝ) (cutoff : ℝ) (level : ℕ) {a b : ℤ} (hab : a ≠ b) :
        Disjoint (g.cellTops tops slope precision cutoff level a)
          (g.cellTops tops slope precision cutoff level b) := by
    …

    Mentions: OAI.LipschitzHilbert.AngularGrid

15. theorem OAI.LipschitzHilbert.AngularGrid.sum_cell_mass_le_boundary line 172

    Source documentation

    A finite collection of child cells included in the boundary consumes at most its mass. In particular this pays for a closed graph neighborhood.

    theorem sum_cell_mass_le_boundary (g : AngularGrid) (tops : Finset ι)
        (slope precision : ι → ℝ) (cutoff : ℝ) (weight : ι → X → ℝ)
        (hw : ∀ i x, 0 ≤ weight i x) (base level : ℕ) (gap s : ℝ) (cells : Finset ℤ)
        (hsub : ∀ c ∈ cells, g.cellTops tops slope precision cutoff (level + 1) c ⊆
          g.boundaryTops tops slope precision cutoff base level gap s) (x : X) :
        (∑ c ∈ cells, g.mass tops slope precision cutoff weight (level + 1) c x) ≤
          g.boundaryMass tops slope precision cutoff weight base level gap s x := by
    …

    Mentions: OAI.LipschitzHilbert.AngularGrid