SourceLatticePacket.lean`

26 declarations, 0 contain sorry, 0 declared as axioms

Actual general planar packets on translated sheared lattices form the canonical planar packet family. Only the bookkeeping sites are quantized: the raw waves retain their original centers and profiles.

structure OAI.LipschitzHilbert.SourceLatticePacket line 20
Source documentation
Concrete local packet data. These are geometric, seminorm and dimensionless scale bounds, with no coefficient or concentration premise.
```
structure SourceLatticePacket (N : ℕ) (κ : Type) (ι : Fin N → Type)
    [Fintype κ] [∀ j, Fintype (ι j)] where
…
```
def OAI.LipschitzHilbert.SourceLatticePacket.length line 56
theorem OAI.LipschitzHilbert.SourceLatticePacket.length_pos line 58
def OAI.LipschitzHilbert.SourceLatticePacket.actualX line 61
def OAI.LipschitzHilbert.SourceLatticePacket.actualZ line 64
def OAI.LipschitzHilbert.SourceLatticePacket.snappedSite line 67
theorem OAI.LipschitzHilbert.SourceLatticePacket.snappedSite_injective line 71
def OAI.LipschitzHilbert.SourceLatticePacket.raw line 74
theorem OAI.LipschitzHilbert.SourceLatticePacket.raw_eq_physical_slice line 81
Source documentation
The center drift is theta-t, whereas the modulation along the reference line has shear t-theta. This identifies every actual raw jet with the corresponding restriction of the physical planar packet.
```
theorem raw_eq_physical_slice (i : Fin 3) (j : Fin N) (u : ι j) (k : κ)
    (y t : ℝ) :
    P.raw i j u k y = planarSchwartzSlice
      (planarCovariantJet (physicalPlanarPacket (P.profile j u k)
        (P.actualX j u) (P.actualZ j u + t * P.actualX j u)
        (P.length j) P.width (t + P.rowSlope j) (P.frequency k)
        (P.length_pos j).ne' P.width_pos.ne') (P.frequency k) P.scale i) y t := by
…
```
Mentions: OAI.LipschitzHilbert.planarSchwartzSlice, OAI.LipschitzHilbert.planarCovariantJet, OAI.LipschitzHilbert.physicalPlanarPacket
def OAI.LipschitzHilbert.SourceLatticePacket.amplitude line 97
def OAI.LipschitzHilbert.SourceLatticePacket.constant line 100
theorem OAI.LipschitzHilbert.SourceLatticePacket.amplitude_pos line 102
theorem OAI.LipschitzHilbert.SourceLatticePacket.constant_pos line 108
theorem OAI.LipschitzHilbert.SourceLatticePacket.raw_shear_bound line 111
theorem OAI.LipschitzHilbert.SourceLatticePacket.raw_carrier_bound line 114
theorem OAI.LipschitzHilbert.SourceLatticePacket.raw_bound_actual line 118
theorem OAI.LipschitzHilbert.SourceLatticePacket.raw_derivative_bound_actual line 128
theorem OAI.LipschitzHilbert.SourceLatticePacket.snapped_envelope line 138
theorem OAI.LipschitzHilbert.SourceLatticePacket.raw_bound line 152
theorem OAI.LipschitzHilbert.SourceLatticePacket.raw_derivative_bound line 160
theorem OAI.LipschitzHilbert.SourceLatticePacket.raw_bound_three line 171
def OAI.LipschitzHilbert.SourceLatticePacket.family line 183
Source documentation
Canonical sites with base coordinates zero, carrying the original raw waves at their actual translated sheared lattice centers.
```
def family : PlanarPacketFamily N κ ι where
…
```
Mentions: OAI.LipschitzHilbert.PlanarPacketFamily
theorem OAI.LipschitzHilbert.SourceLatticePacket.family_length line 204
theorem OAI.LipschitzHilbert.SourceLatticePacket.family_wave line 206
theorem OAI.LipschitzHilbert.SourceLatticePacket.family_centerX line 209
theorem OAI.LipschitzHilbert.SourceLatticePacket.family_centerZ line 214