SourceLatticePolarizationSpectrum.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Polarization preserves the original physical packet spectrum. Both profiles use the same carrier and geometry, so their linear combination has no Fourier support outside their shared wedge and band.

theorem OAI.LipschitzHilbert.physicalPlanarPacket_add_smul line 15
theorem OAI.LipschitzHilbert.planarFourier_add line 24
theorem OAI.LipschitzHilbert.planarAngularFourier_add_smul line 32
theorem OAI.LipschitzHilbert.SourceLatticePacket.polarize_physicalPacket line 46
theorem OAI.LipschitzHilbert.SourceLatticePacket.polarize_physicalFourier line 59

theorem OAI.LipschitzHilbert.SourceLatticePacket.polarize_physicalFourier_eq_zero line 67

Source documentation

Every zero shared by the two original physical spectra is retained.

theorem polarize_physicalFourier_eq_zero (c : ℂ) (hc : ‖c‖ = 1)
    (t : ℝ) (j : Fin N) (u : ι j) (k : κ) (ξ η : ℝ)
    (hp : planarAngularFourier (P.physicalPacket t j u k) (ξ, η) = 0)
    (hq : planarAngularFourier ((P.withProfile alt hAlt).physicalPacket t j u k) (ξ, η) = 0) :
    planarAngularFourier ((P.polarize alt hAlt c hc).physicalPacket t j u k) (ξ, η) = 0 := by
…

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

theorem OAI.LipschitzHilbert.SourceLatticePacket.polarize_spectrum line 76

Source documentation

The original wedge and positive vertical band are sufficient for all four polarization families; no additional support hypothesis is used.

theorem polarize_spectrum (c : ℂ) (hc : ‖c‖ = 1)
    (t w cStar cEta CEta : ℝ)
    (hp : ∀ j u k ξ η, planarAngularFourier (P.physicalPacket t j u k) (ξ, η) ≠ 0 →
      |ξ + (t + P.rowSlope j) * η| ≤ cStar / P.length j ∧
        cEta ≤ w * η ∧ w * η ≤ CEta)
    (hq : ∀ j u k ξ η,
      planarAngularFourier ((P.withProfile alt hAlt).physicalPacket t j u k) (ξ, η) ≠ 0 →
      |ξ + (t + P.rowSlope j) * η| ≤ cStar / P.length j ∧
        cEta ≤ w * η ∧ w * η ≤ CEta) :
    ∀ j u k ξ η,
      planarAngularFourier ((P.polarize alt hAlt c hc).physicalPacket t j u k) (ξ, η) ≠ 0 →
      |ξ + (t + P.rowSlope j) * η| ≤ cStar / P.length j ∧
…

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