SourceTerminalScale.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The least ineligible shifted endpoint provides a finite terminal generation without enlarging the source root line window past its top. This includes exactly one final block after the last eligible endpoint.

def OAI.LipschitzHilbert.AngularGrid.firstIneligibleShiftedBlock line 16
theorem OAI.LipschitzHilbert.AngularGrid.firstIneligibleShiftedBlock_spec line 20
theorem OAI.LipschitzHilbert.AngularGrid.eligible_before_firstIneligibleShiftedBlock line 26
theorem OAI.LipschitzHilbert.AngularGrid.eligible_iff_lt_firstIneligibleShiftedBlock line 33
theorem OAI.LipschitzHilbert.AngularGrid.firstIneligibleShiftedBlock_pos line 46
theorem OAI.LipschitzHilbert.AngularGrid.source_block_line_scale_le_length line 59
Source documentation
Even the terminal block, whose upper endpoint need no longer be eligible, has line window at most the original top length. Eligibility is only used at the lower endpoint and the block width jump is at most B.
```
theorem source_block_line_scale_le_length (g : AngularGrid) (L : ℝ)
    (hbranch : (g.branching:ℝ) = SourceParameters.step L)
    (hK : 0 < SourceParameters.blockCount L) (σ : Fin (SourceParameters.blockCount L))
    (j : ℕ) {w length : ℝ} (hw : 0 < w) (hlength : 0 < length)
    (he : g.eligible (g.rootWidth/(SourceParameters.branching L)^2) (w/length)
      (ShiftedBlocks.endpoint σ j)) :
    sourceLineScale g L w (ShiftedBlocks.endpoint σ (j+1)) ≤ length := by
…
```
Mentions: OAI.LipschitzHilbert.AngularGrid, OAI.LipschitzHilbert.SourceParameters.step, OAI.LipschitzHilbert.SourceParameters.blockCount, OAI.LipschitzHilbert.SourceParameters.branching, OAI.LipschitzHilbert.ShiftedBlocks.endpoint, OAI.LipschitzHilbert.sourceLineScale

theorem OAI.LipschitzHilbert.AngularGrid.source_first_terminal_grid_width line 98

Source documentation

The concrete reverse grid ending at the first ineligible endpoint satisfies the width hypothesis of the weighted path integral.

theorem source_first_terminal_grid_width (g : AngularGrid) (L origin : ℝ)
    (hbranch : (g.branching:ℝ) = SourceParameters.step L)
    (hK : 0 < SourceParameters.blockCount L) (σ : Fin (SourceParameters.blockCount L))
    {w length : ℝ} (hw : 0 < w) (hlength : 0 < length)
    (hzero : g.eligible (g.rootWidth/(SourceParameters.branching L)^2) (w/length) 0) :
    let count := g.firstIneligibleShiftedBlock (g.rootWidth/(SourceParameters.branching L)^2)
…

Mentions: OAI.LipschitzHilbert.AngularGrid, OAI.LipschitzHilbert.SourceParameters.step, OAI.LipschitzHilbert.SourceParameters.blockCount, OAI.LipschitzHilbert.SourceParameters.branching