SourceBoundaryScales.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The manuscript's boundary radius is G^(-1/4) times the parent width. At a last transition this is exactly G^(3/4) times the child width.

def OAI.LipschitzHilbert.AngularGrid.sourceBoundaryGap line 12
theorem OAI.LipschitzHilbert.AngularGrid.sourceBoundaryGap_pos line 15
theorem OAI.LipschitzHilbert.AngularGrid.sourceBoundaryGap_le_width line 19
theorem OAI.LipschitzHilbert.AngularGrid.sourceBoundaryGap_eq_sourceGap line 25

theorem OAI.LipschitzHilbert.AngularGrid.source_shifted_boundary_mass line 44

Source documentation

The boundary mass in the shared analytic family is exactly the neighborhood mass used in the shifted block's graph predictor.

theorem source_shifted_boundary_mass {ι X : Type*}
    (g : AngularGrid) (L : ℝ) (hbranch : (g.branching:ℝ) = SourceParameters.step L)
    (tops : Finset ι) (slope precision : ι → ℝ) (cutoff : ℝ) (weight : ι → X → ℝ)
    (hK : 0 < SourceParameters.blockCount L) (σ : Fin (SourceParameters.blockCount L))
    (j : ℕ) (s : ℝ) (x : X) :
    g.sourceBoundaryMass tops slope precision cutoff weight (SourceParameters.blockCount L)
      (g.sourceBoundaryGap L) (ShiftedBlocks.lastTransition σ j)
      (g.index (ShiftedBlocks.endpoint σ (j+1)) s) x =
    g.boundaryMass tops slope precision cutoff weight (ShiftedBlocks.endpoint σ j)
      (ShiftedBlocks.lastTransition σ j) (g.sourceGap L (ShiftedBlocks.endpoint σ (j+1))) s x := by
…

Mentions: OAI.LipschitzHilbert.AngularGrid, OAI.LipschitzHilbert.SourceParameters.step, OAI.LipschitzHilbert.SourceParameters.blockCount, OAI.LipschitzHilbert.ShiftedBlocks.lastTransition, OAI.LipschitzHilbert.ShiftedBlocks.endpoint