SourceSlottedLattice.lean`

25 declarations, 0 contain sorry, 0 declared as axioms

Actual source lattices with several labels at each scale split into the uniformly many slots constructed in SourceSlopeLabels. No packets are inserted at an empty scale. The selected profiles, physical centers, carrier frequencies and spectra are unchanged.

structure OAI.LipschitzHilbert.SourceLabeledLattice line 21
Source documentation
Common packet bounds with a finite set of translated lattice labels at each scale. All bounds are imposed only on labels that are present.
```
structure SourceLabeledLattice (N : ℕ) (κ : Type) (Label : Fin N → Type)
    (Item : ∀ j, Label j → Type) [Fintype κ] [∀ j l, Fintype (Item j l)] where
…
```
def OAI.LipschitzHilbert.SourceLabeledLattice.length line 58
theorem OAI.LipschitzHilbert.SourceLabeledLattice.length_pos line 60
def OAI.LipschitzHilbert.SourceLabeledLattice.actualX line 63
def OAI.LipschitzHilbert.SourceLabeledLattice.actualZ line 66
def OAI.LipschitzHilbert.SourceLabeledLattice.raw line 70
def OAI.LipschitzHilbert.SourceLabeledLattice.physicalPacket line 75
def OAI.LipschitzHilbert.SourceLabeledLattice.constant line 81
def OAI.LipschitzHilbert.SourceLabeledLattice.slotEmbedding line 87
abbrev OAI.LipschitzHilbert.SourceLabeledLattice.SlotItem line 89
instance OAI.LipschitzHilbert.SourceLabeledLattice.slotItemFintype line 92
def OAI.LipschitzHilbert.SourceLabeledLattice.slotItemsEquiv line 97
Source documentation
Every original item occurs in exactly one slot.
```
def slotItemsEquiv (j : Fin N) :
    (Σ b : Fin B, P.SlotItem hcard b j) ≃ Σ l : P.labels j, Item j l where
…
```

theorem OAI.LipschitzHilbert.SourceLabeledLattice.sum_slotted line 109

Source documentation

Splitting by slots is an exact identity for arbitrary finite packet sums, not an estimate and not a change to the waves.

theorem sum_slotted {E : Type*} [AddCommMonoid E] (j : Fin N)
    (f : ∀ l : P.labels j, Item j l → E) :
    (∑ b : Fin B, ∑ p : P.SlotItem hcard b j, f p.1.1 p.1.2) =
      ∑ l : P.labels j, ∑ u : Item j l, f l u := by
…

def OAI.LipschitzHilbert.SourceLabeledLattice.slotValue line 121
Source documentation
The value is used only when the corresponding slot has an item. Zero is a harmless geometric default when that slot is empty.
```
def slotValue (b : Fin B) (j : Fin N) (f : P.labels j → ℝ) : ℝ :=
…
```
theorem OAI.LipschitzHilbert.SourceLabeledLattice.slotValue_item line 124
def OAI.LipschitzHilbert.SourceLabeledLattice.slotted line 132
Source documentation
One genuine translated-lattice family per slot. No hypotheses on a selector are introduced for missing labels or empty scales.
```
def slotted (b : Fin B) : SourceLatticePacket N κ (P.SlotItem hcard b) where
…
```
Mentions: OAI.LipschitzHilbert.SourceLatticePacket
theorem OAI.LipschitzHilbert.SourceLabeledLattice.slotted_length line 167
theorem OAI.LipschitzHilbert.SourceLabeledLattice.slotted_constant line 170
theorem OAI.LipschitzHilbert.SourceLabeledLattice.slotted_actualX line 173
theorem OAI.LipschitzHilbert.SourceLabeledLattice.slotted_actualZ line 179
theorem OAI.LipschitzHilbert.SourceLabeledLattice.slotted_rowSlope line 188
theorem OAI.LipschitzHilbert.SourceLabeledLattice.slotted_raw line 192
theorem OAI.LipschitzHilbert.SourceLabeledLattice.slotted_physicalPacket line 200
theorem OAI.LipschitzHilbert.SourceLabeledLattice.slotted_spectrum line 208

theorem OAI.LipschitzHilbert.SourceLabeledLattice.slotted_selector line 223

Source documentation

Selector separation is only needed for existing packets; therefore it is inherited even when a slot is empty at some scales.

theorem slotted_selector (w cb Cb : ℝ)
    (hselector : ∀ j (l : P.labels j) (_u : Item j l),
      cb * w / P.length j ≤ |P.rowSlope j l| ∧
        |P.rowSlope j l| ≤ Cb * w / P.length j)
    (b : Fin B) (j : Fin N) (p : P.SlotItem hcard b j) :
    cb * w / (P.slotted hcard b).length j ≤ |(P.slotted hcard b).rowSlope j| ∧
      |(P.slotted hcard b).rowSlope j| ≤ Cb * w / (P.slotted hcard b).length j := by
…

Mentions: OAI.LipschitzHilbert.SourceLabeledLattice.length