SourceReferenceLattice.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Change the reference direction of an actual translated source lattice. Profiles, sites and physical packets are preserved exactly. The reference-cone and width hypotheses imply the new shear and carrier bounds; the absolute raw envelope is independent of the carrier bound.

def OAI.LipschitzHilbert.SourceLatticePacket.changeReference line 19
theorem OAI.LipschitzHilbert.SourceLatticePacket.changeReference_length line 35
theorem OAI.LipschitzHilbert.SourceLatticePacket.changeReference_actualX line 38
theorem OAI.LipschitzHilbert.SourceLatticePacket.changeReference_actualZ line 41
theorem OAI.LipschitzHilbert.SourceLatticePacket.changeReference_physicalPacket line 49
Source documentation
The new reference slope is t; the old one is t+delta. There is no change to the original two-dimensional packet.
```
theorem changeReference_physicalPacket (t : ℝ) (j : Fin N) (u : ι j) (k : κ) :
    (P.changeReference delta M hM hshear hcarrier).physicalPacket t j u k =
      P.physicalPacket (t+delta) j u k := by
…
```
Mentions: OAI.LipschitzHilbert.SourceLatticePacket.physicalPacket
theorem OAI.LipschitzHilbert.SourceLatticePacket.changeReference_raw_slice line 67

theorem OAI.LipschitzHilbert.SourceLatticePacket.reference_cone_bounds line 80

Source documentation

The cone needed for reference-line packets implies both analytic dimensionless bounds, using only the original width and frequency scale.

theorem reference_cone_bounds {delta H F w : ℝ} (hw : 0 < w)
    (_hH : 0 ≤ H) (hF : 0 ≤ F) (hwide : H*w ≤ P.width)
    (hcone : ∀ j, |P.rowSlope j+delta| ≤ H*w/P.length j)
    (hfrequency : ∀ k, |P.frequency k| ≤ F/w) :
    (∀ j, |(P.rowSlope j+delta)*P.length j/P.width| ≤ 1) ∧
      ∀ j k, |P.frequency k*(P.rowSlope j+delta)*P.length j| ≤ F*H := by
…

theorem OAI.LipschitzHilbert.SourceLatticePacket.raw_absolute_envelope line 101

Source documentation

Unlike derivative bounds, the raw absolute envelope has no carrier factor, even when the reference cone is much wider than a main annulus.

theorem raw_absolute_envelope (i : Fin 3) (j : Fin N) (u : ι j) (k : κ) (y x : ℝ) :
    ‖P.raw i j u k y x‖ ≤
      ((2^P.order*P.profileBound)*P.ratioBound^2)*
        (lineEnvelope (P.actualX j u) (P.length j) P.order x*
          lineEnvelope (P.actualZ j u) P.width P.order y) := by
…

Mentions: OAI.LipschitzHilbert.lineEnvelope

theorem OAI.LipschitzHilbert.SourceLatticePacket.changeReference_fourier_cutoffs line 124

Source documentation

Fourier annuli on the new reference line follow from the spectrum of the unchanged original physical packet, including all three jets.

theorem changeReference_fourier_cutoffs (t w cStar cEta CEta cb Cb : ℝ)
    (hw : 0 < w) (hcEta : 0 < cEta) (hcb : 0 ≤ cb) (hCb : 0 ≤ Cb)
    (hspectrum : ∀ j u k ξ η, planarAngularFourier (P.physicalPacket (t+delta) j u k) (ξ,η) ≠ 0 →
      |ξ+((t+delta)+P.rowSlope j)*η| ≤ cStar/P.length j ∧
        cEta ≤ w*η ∧ w*η ≤ CEta)
    (hselector : ∀ j (_u : ι j), cb*w/P.length j ≤ |P.rowSlope j+delta| ∧
      |P.rowSlope j+delta| ≤ Cb*w/P.length j)
    (i : Fin 3) (j : Fin N) (u : ι j) (k : κ) (y : ℝ) :
    (∀ ξ, |ξ| < (((cEta*cb-cStar)/(2*Real.pi))/P.topLength)*(2:ℝ)^j.val →
      𝓕 ((P.changeReference delta M hM hshear hcarrier).raw i j u k y) ξ = 0) ∧
    (∀ ξ, (((CEta*Cb+cStar)/(2*Real.pi))/P.topLength)*(2:ℝ)^j.val < |ξ| →
      𝓕 ((P.changeReference delta M hM hshear hcarrier).raw i j u k y) ξ = 0) := by
…

Mentions: OAI.LipschitzHilbert.planarAngularFourier, OAI.LipschitzHilbert.SourceLatticePacket.raw