SourceLabeledMainRestriction.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Only nonzero frozen selectors enter the positive main scale. Restricting to their fixed narrow reference cone is exact, and changes the carrier bound without changing any retained physical packet or positive envelope. The wide error family is not used in the main tail.

theorem OAI.LipschitzHilbert.SourceLabeledLattice.physicalFrozenCenteredCoefficient_eq_zero line 19
theorem OAI.LipschitzHilbert.SourceLabeledLattice.referenceSelf_constant line 36
Source documentation
The retained main family pays only the narrow cone's carrier bound. Its absolute envelope constant is unchanged.
```
theorem referenceSelf_constant :
    (Q).constant = P.absoluteConstant*(F*cone+2) := by
…
```
Mentions: OAI.LipschitzHilbert.SourceLabeledLattice.constant
theorem OAI.LipschitzHilbert.SourceLabeledLattice.referenceSelf_absoluteConstant line 41
theorem OAI.LipschitzHilbert.SourceLabeledLattice.referenceSelf_snappedSite line 43
theorem OAI.LipschitzHilbert.SourceLabeledLattice.referenceSelf_positiveEnvelope line 51
theorem OAI.LipschitzHilbert.SourceLabeledLattice.referenceSelf_frozenCenteredCoefficient line 58

theorem OAI.LipschitzHilbert.SourceLabeledLattice.physicalMainScale_eq_narrow_reference line 82

Source documentation

The positive main scale may be restricted to the narrow fixed reference family before any probabilistic or variational estimate.

theorem physicalMainScale_eq_narrow_reference (a : ℝ)
    (b : ∀ j, P.labels j → κ → ℝ → ℂ)
    (v : ℝ×ℝ → ℝ) (g : ℝ×ℝ → EuclideanSpace ℂ κ)
    (hshort : ∀ j l k, b j l k t ≠ 0 → P.length j ≤ R)
    (hsupport : ∀ j l k, b j l k t ≠ 0 → |t+P.rowSlope j l-t| ≤ cone*w/P.length j)
    (j : Fin N) (y x : ℝ) :
    P.physicalMainScale t a b v g j y x =
      (Q).physicalMainScale t a (fun j l k s => b j (orig j l) k s) v g j y x := by
…

Mentions: OAI.LipschitzHilbert.SourceLabeledLattice.physicalMainScale

theorem OAI.LipschitzHilbert.SourceLabeledLattice.physicalMainSquare_eq_narrow_reference line 111
theorem OAI.LipschitzHilbert.SourceLabeledLattice.referenceSelf_alt_physicalPacket line 123

theorem OAI.LipschitzHilbert.SourceLabeledLattice.physicalCenteredMaskedBand_eq_narrow_reference line 135

Source documentation

The same exact narrow restriction holds for the masked main synthesis, retaining the alternate profile and each original top mask.

theorem physicalCenteredMaskedBand_eq_narrow_reference
    (alt : ∀ j (l : P.labels j), Item j l → κ → SchwartzMap (ℝ×ℝ) ℂ)
    (hAlt : ∀ j l u k, planarProfileConstant (alt j l u k) (2*P.order) ≤ P.profileBound)
    (a : ℝ) (b : ∀ j, P.labels j → κ → ℝ → ℂ)
    (v : ℝ×ℝ → ℝ) (g : ℝ×ℝ → EuclideanSpace ℂ κ)
    (T : ∀ j (l : P.labels j), Item j l → SlopeBox) (L A y : ℝ)
    (hshort : ∀ j l k, b j l k t ≠ 0 → P.length j ≤ R)
    (hsupport : ∀ j l k, b j l k t ≠ 0 → |t+P.rowSlope j l-t| ≤ cone*w/P.length j)
    (j : Fin N) (x : ℝ) :
    P.physicalCenteredMaskedBand alt hAlt t a b v g T L A y j x =
      (Q).physicalCenteredMaskedBand (fun j l u k => alt j (orig j l) u k)
        (fun j l u k => hAlt j (orig j l) u k) t a
…

Mentions: OAI.LipschitzHilbert.planarProfileConstant, OAI.LipschitzHilbert.SlopeBox, OAI.LipschitzHilbert.SourceLabeledLattice.physicalCenteredMaskedBand

theorem OAI.LipschitzHilbert.SourceLabeledLattice.physicalCenteredMaskedVariation_eq_narrow_reference line 176