OAI/Analysis/LipschitzHilbert/Packets/PacketDataParentResidualReference.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LipschitzHilbert.PacketLatticeData.short_parent_residual_eq line 16

   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 : PacketLatticeData 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.PacketLatticeData, OAI.LipschitzHilbert.AngularGrid