OAI/Analysis/LipschitzHilbert/Packets/SourceSupportedLabeledGeometry.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Packetwise top geometry survives slotting and frozen-active label restriction. These operations keep every retained center and length.

  1. theorem OAI.LipschitzHilbert.SourceLabeledLattice.supportedTopGeometry line 17

    Source documentation

    The actual packet-center condition already controls retained lengths.

    theorem supportedTopGeometry {T : SlopeBox} {K : ℝ} {D : ℕ}
    (hwidth : P.width ≤ K*T.width)
    (hx : ∀ j l u, |P.actualX j l u-T.x|+P.length j ≤ K*T.length)
    (hz : ∀ j l u, |P.actualZ j l u-(T.y-T.slope*T.x)|+P.width ≤ K*T.width)
    (horder : 3+2*(8*D+1) ≤ P.order) (hscale : P.scale = 4*(K*T.width)) :
    SourceSupportedLabeledTopGeometry P T K D where
…

    Mentions: OAI.LipschitzHilbert.SlopeBox, OAI.LipschitzHilbert.SourceSupportedLabeledTopGeometry

  2. theorem OAI.LipschitzHilbert.SourceLabeledLattice.slotted_supportedTopGeometry line 30
  3. theorem OAI.LipschitzHilbert.SourceLabeledLattice.activeMainFamily_supportedTopGeometry line 47