SourceResidualGeometry.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The fixed residual packet collection uses only endpoints at which the reference top is still eligible. Its packets are shorter than that top and lie in the reference angular cone. These are the geometric hypotheses of the existing reference-line variation estimate.

theorem OAI.LipschitzHilbert.AngularGrid.not_eligible_above_lastEligible line 16
theorem OAI.LipschitzHilbert.AngularGrid.lastEligible_antitone_precision_global line 26
Source documentation
The definition with natural subtraction stays monotone even at empty scales that were already ineligible at level zero.
```
theorem lastEligible_antitone_precision_global (g : AngularGrid) (cutoff p q : ℝ)
    (hp : 0 < p) (hq : 0 < q) (hpq : p ≤ q) :
    g.lastEligible cutoff q hq ≤ g.lastEligible cutoff p hp := by
…
```
Mentions: OAI.LipschitzHilbert.AngularGrid
theorem OAI.LipschitzHilbert.AngularGrid.source_length_stopping_antitone line 37

theorem OAI.LipschitzHilbert.AngularGrid.source_length_residual_variation line 48

Source documentation

The precise source stopping map may replace the abstract antitone map in the already proved cubic-variation bridge.

theorem source_length_residual_variation {σ E : Type*} [NormedAddCommGroup E]
    {N : ℕ} (g : AngularGrid) (cutoff : ℝ) {w : ℝ} (hw : 0 < w)
    (length : Fin N → ℝ) (hlen : ∀ j, 0 < length j) (horder : Antitone length)
    (Q : Finset σ) (lengthIndex : σ → Fin N) (value : σ → E) (H : ℕ) :
    let stop := fun j => g.lastEligible cutoff (w/length j) (div_pos hw (hlen j))
…

Mentions: OAI.LipschitzHilbert.AngularGrid

theorem OAI.LipschitzHilbert.AngularGrid.residual_packet_length_and_cone line 61

Source documentation

A shorter stopping time means a strictly shorter physical packet than any reference length still eligible at the block endpoint.

theorem residual_packet_length_and_cone (g : AngularGrid)
    {w B packetLength referenceLength C packetSlope assignedSlope referenceSlope : ℝ}
    (hw : 0 < w) (hB : 0 < B) (hp : 0 < packetLength) (hR : 0 < referenceLength)
    (hzero : g.eligible (g.rootWidth/B^2) (w/packetLength) 0)
    {upper : ℕ}
    (hstop : g.lastEligible (g.rootWidth/B^2) (w/packetLength) (div_pos hw hp) < upper)
    (hreference : g.eligible (g.rootWidth/B^2) (w/referenceLength) upper)
    (hcell : g.index upper assignedSlope = g.index upper referenceSlope)
    (hangle : |packetSlope-assignedSlope| ≤ C*(w/packetLength)) :
    packetLength < referenceLength ∧
      |packetSlope-referenceSlope| ≤ (C+B^2)*(w/packetLength) := by
…

Mentions: OAI.LipschitzHilbert.AngularGrid

theorem OAI.LipschitzHilbert.AngularGrid.fixedPathResidualPackets_geometry line 99

Source documentation

Membership in the actual fixed residual collection supplies the child-cell condition and the strictly later eligible endpoint.

theorem fixedPathResidualPackets_geometry {ι σ : Type*} (g : AngularGrid)
    (tops : Finset ι) (slope precision : ι → ℝ) (packets : Finset σ)
    (assigned : σ → ι) (length angle : σ → ℝ) (hlen : ∀ q, 0 < length q)
    {w B referenceLength C : ℝ} (hw : 0 < w) (hB : 0 < B) (hR : 0 < referenceLength)
    (level : ℕ → ℕ) (count : ℕ) (pathTop : ι)
    (hprecision : precision pathTop = w/referenceLength)
    (hreference : ∀ j < count, g.eligible (g.rootWidth/B^2) (precision pathTop) (level (j+1)))
    (hzero : ∀ q ∈ packets, g.eligible (g.rootWidth/B^2) (w/length q) 0)
    (hangle : ∀ q ∈ packets, |angle q-slope (assigned q)| ≤ C*(w/length q))
    {q : σ}
    (hq : q ∈ g.fixedPathResidualPackets tops slope precision (g.rootWidth/B^2)
      packets assigned (fun q => g.lastEligible (g.rootWidth/B^2) (w/length q)
…

Mentions: OAI.LipschitzHilbert.AngularGrid

theorem OAI.LipschitzHilbert.AngularGrid.shifted_residual_collection_geometry line 124

Source documentation

The source uses all and only blocks preceding its first ineligible endpoint. Thus the residual family is fixed before mass stopping or evaluation of any spatial point.

theorem shifted_residual_collection_geometry {ι σ : Type*} {K : ℕ}
    (g : AngularGrid) (tops : Finset ι) (slope precision : ι → ℝ)
    (packets : Finset σ) (assigned : σ → ι) (length angle : σ → ℝ)
    (hlen : ∀ q, 0 < length q)
    {w B referenceLength C : ℝ} (hw : 0 < w) (hB : 0 < B) (hR : 0 < referenceLength)
    (hK : 0 < K) (shift : Fin K) (pathTop : ι)
    (hprecision : precision pathTop = w/referenceLength)
    (hzero : ∀ q ∈ packets, g.eligible (g.rootWidth/B^2) (w/length q) 0)
    (hangle : ∀ q ∈ packets, |angle q-slope (assigned q)| ≤ C*(w/length q)) :
    let terminal := g.firstIneligibleShiftedBlock (g.rootWidth/B^2) (w/referenceLength)
…

Mentions: OAI.LipschitzHilbert.AngularGrid