SourceLabeledMainSlots.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The positive frozen main sum in the original labeled collection is exactly the sum of the centered positive scales in its fixed slots. The physical packets, coefficients and snapped envelopes are unchanged.

theorem OAI.LipschitzHilbert.SourceLabeledLattice.slotted_snappedSite line 20
theorem OAI.LipschitzHilbert.SourceLabeledLattice.slotted_positiveEnvelope line 30
def OAI.LipschitzHilbert.SourceLabeledLattice.frozenSlot line 37
theorem OAI.LipschitzHilbert.SourceLabeledLattice.frozenSlot_positiveEnvelope line 43

theorem OAI.LipschitzHilbert.SourceLabeledLattice.frozenSlot_physicalCenteredCoefficient line 52

Source documentation

Slotting and freezing reproduce the original centered physical coefficient, with no integral or cutoff-boundary exception.

theorem frozenSlot_physicalCenteredCoefficient (t a : ℝ)
    (b : ∀ j, P.labels j → κ → ℝ → ℂ) (hb : ∀ j l k, ‖b j l k t‖ ≤ 1)
    (v : ℝ×ℝ → ℝ) (g : ℝ×ℝ → EuclideanSpace ℂ κ)
    (s : Fin B) (j : Fin N) (p : P.SlotItem hcard s j) :
    (P.frozenSlot hcard t b hb s).physicalCenteredCoefficient t t
        (fun j => a*(2:ℝ)^j.val) v g j p =
      P.physicalFrozenCenteredCoefficient t a b v g j p.1.1 p.1.2 := by
…

theorem OAI.LipschitzHilbert.SourceLabeledLattice.physicalMainScale_eq_slots line 77

Source documentation

The original main positive scale is a literal fixed-slot sum.

theorem physicalMainScale_eq_slots (t a : ℝ)
    (b : ∀ j, P.labels j → κ → ℝ → ℂ) (hb : ∀ j l k, ‖b j l k t‖ ≤ 1)
    (v : ℝ×ℝ → ℝ) (g : ℝ×ℝ → EuclideanSpace ℂ κ) (j : Fin N) (y x : ℝ) :
    P.physicalMainScale t a b v g j y x =
      ∑ s : Fin B, (P.frozenSlot hcard t b hb s).physicalCenteredPositiveScale
        t t (fun j => a*(2:ℝ)^j.val) v g j y x := by
…

theorem OAI.LipschitzHilbert.SourceLabeledLattice.physicalMainSquare_le_slots line 102

Source documentation

The exact identity supplies the square domination consumed by the fixed-slot physical tail theorem.

theorem physicalMainSquare_le_slots (t a : ℝ)
    (b : ∀ j, P.labels j → κ → ℝ → ℂ) (hb : ∀ j l k, ‖b j l k t‖ ≤ 1)
    (v : ℝ×ℝ → ℝ) (g : ℝ×ℝ → EuclideanSpace ℂ κ) (y x : ℝ) :
    Real.sqrt (∑ j, P.physicalMainScale t a b v g j y x^2) ≤
      ∑ s : Fin B, (P.frozenSlot hcard t b hb s).physicalCenteredSquare
        t t (fun j => a*(2:ℝ)^j.val) v g y x := by
…