SourceParentResidualReference.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

A square estimate uses the parent residual cone. Its exact packet restriction can be recentered at the path slope; no equality with the original reference slope is required.

theorem OAI.LipschitzHilbert.AngularGrid.packetResidual_eq_of_support_subset line 14

theorem OAI.LipschitzHilbert.SourceLabeledLattice.short_parent_residual_eq line 43

Source documentation

Every actual short residual is unchanged after restriction to the fixed parent cone. This includes the terminal block.

theorem short_parent_residual_eq {τ E : Type*} [AddCommMonoid E] [Module ℂ E]
    (P : SourceLabeledLattice N κ Label Item) (grid : AngularGrid)
    (packets : Finset P.PacketIndex) (assigned : P.PacketIndex → τ) (slope : τ → ℝ)
    (t R C B w : ℝ) (hw : 0 < w) (hB : 0 < B)
    (hzero : ∀ j, grid.eligible (grid.rootWidth/B^2) (w/P.length j) 0)
    (hangle : ∀ q ∈ packets,
      |t+P.rowSlope q.1 q.2.1-slope (assigned q)| ≤ C*(w/P.length q.1))
    (base : P.PacketIndex → E) (transition : ℕ → ℤ → ℂ)
    (lower upper : ℕ) (pathSlope : ℝ)
    (hwidth : grid.width lower ≤ B*grid.width upper) :
    let stop := fun q : P.PacketIndex => grid.lastEligible (grid.rootWidth/B^2)
…

Mentions: OAI.LipschitzHilbert.SourceLabeledLattice, OAI.LipschitzHilbert.AngularGrid