OAI/Analysis/LipschitzHilbert/Trees/SourceResidualBlockGeometry.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LipschitzHilbert.dyadic_precision_band_card line 16
2. def OAI.LipschitzHilbert.residualLengthSet line 44
3. theorem OAI.LipschitzHilbert.residualLengthSet_disjoint line 47
4. theorem OAI.LipschitzHilbert.AngularGrid.source_residual_precision_window line 60
5. theorem OAI.LipschitzHilbert.AngularGrid.source_parent_residual_cone line 80

   Source documentation

   The full residual only belongs to the parent cell. Its cone is wider by one block ratio than the continuing residual's cone.

   theorem source_parent_residual_cone (g : AngularGrid)
       {w B length C packetSlope assignedSlope referenceSlope : ℝ}
       (hw : 0 < w) (hB : 0 < B) (hlen : 0 < length)
       (hzero : g.eligible (g.rootWidth/B^2) (w/length) 0)
       {lower upper : ℕ}
       (hstop : lower ≤ g.lastEligible (g.rootWidth/B^2) (w/length) (div_pos hw hlen) ∧
         g.lastEligible (g.rootWidth/B^2) (w/length) (div_pos hw hlen) < upper)
       (hwidth : g.width lower ≤ B*g.width upper)
       (hcell : g.index lower assignedSlope = g.index lower referenceSlope)
       (hangle : |packetSlope-assignedSlope| ≤ C*(w/length)) :
       |packetSlope-referenceSlope| ≤ (C+B^3)*(w/length) := by
   …

   Mentions: OAI.LipschitzHilbert.AngularGrid

6. theorem OAI.LipschitzHilbert.AngularGrid.source_residual_length_card line 108

   Source documentation

   A residual block has at most log₂(block ratio) dyadic lengths. The strict lower precision cutoff also handles a zero-width empty band.

   theorem source_residual_length_card {N : ℕ} (g : AngularGrid)
       {w B baseLength : ℝ} (hw : 0 < w) (hB : 0 < B) (hlen : 0 < baseLength)
       (lower upper R : ℕ) (hwidth : g.width lower ≤ (2:ℝ)^R*g.width upper)
       (hzero : ∀ j : Fin N, g.eligible (g.rootWidth/B^2) (w/(baseLength/(2:ℝ)^j.val)) 0) :
       let stop := fun j : Fin N => g.lastEligible (g.rootWidth/B^2)
   …

   Mentions: OAI.LipschitzHilbert.AngularGrid

7. theorem OAI.LipschitzHilbert.AngularGrid.source_shifted_residual_length_card line 131