SourceLabeledMaskedSlots.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Masked centered synthesis in the original labeled family is the exact sum of its fixed-slot syntheses. In particular the cubic variation is controlled by the actual centered masked variations already bounded on physical intervals. No total-label factor occurs.

def OAI.LipschitzHilbert.SourceLabeledLattice.physicalCenteredMaskedBand line 24
def OAI.LipschitzHilbert.SourceLabeledLattice.physicalCenteredMaskedVariation line 30
theorem OAI.LipschitzHilbert.SourceLabeledLattice.physicalCenteredMaskedBand_continuous line 34
theorem OAI.LipschitzHilbert.SourceLabeledLattice.physicalCenteredMaskedVariation_continuous line 48
theorem OAI.LipschitzHilbert.SourceLabeledLattice.physicalCenteredMaskedBand_physical_continuous line 62
Source documentation
Joint continuity in the original physical point, before selecting a reference line or interval.
```
theorem physicalCenteredMaskedBand_physical_continuous (j : Fin N) :
    Continuous (fun z : ℝ×ℝ => P.physicalCenteredMaskedBand
      alt hAlt t a b v g T L A (z.2-t*z.1) j z.1) := by
…
```
theorem OAI.LipschitzHilbert.SourceLabeledLattice.physicalCenteredMaskedVariation_physical_continuous line 77
def OAI.LipschitzHilbert.SourceLabeledLattice.slotCenteredMaskedBand line 95
Source documentation
The slot functions use the original alternate packet and original mask at each retained item.
```
def slotCenteredMaskedBand (s : Fin B) (j : Fin N) (x : ℝ) : EuclideanSpace ℂ κ :=
…
```
theorem OAI.LipschitzHilbert.SourceLabeledLattice.slotCenteredMaskedBand_apply line 103

theorem OAI.LipschitzHilbert.SourceLabeledLattice.physicalCenteredMaskedBand_eq_slots line 127

Source documentation

Exact synthesis recombination, prior to taking any norm.

theorem physicalCenteredMaskedBand_eq_slots (j : Fin N) (x : ℝ) :
    P.physicalCenteredMaskedBand alt hAlt t a b v g T L A y j x =
      ∑ s : Fin B, P.slotCenteredMaskedBand alt hAlt t a b v g T L A y hcard s j x := by
…

theorem OAI.LipschitzHilbert.SourceLabeledLattice.physicalCenteredMaskedVariation_le_slots line 142
Source documentation
Cubic variation is taken only after restoring the original labeled packet sum, and costs the fixed sum of slot variations.
```
theorem physicalCenteredMaskedVariation_le_slots (x : ℝ) :
    P.physicalCenteredMaskedVariation alt hAlt t a b v g T L A y x ≤
      ∑ s : Fin B, cubicVariation
        (packetPartialSum (fun j => P.slotCenteredMaskedBand
          alt hAlt t a b v g T L A y hcard s j x)) N := by
…
```
Mentions: OAI.LipschitzHilbert.cubicVariation, OAI.LipschitzHilbert.packetPartialSum