SourceSelectorConcentrationJets.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Unmasked reference moments for all three original covariant jets. Only the synthesis waves change. The frozen original analyzing coefficient and its proved local budget are retained exactly.

def OAI.LipschitzHilbert.SourceLatticePacket.rawJetFamily line 19
Source documentation
All raw jets have the same lattice and fixed envelope constant.
```
def rawJetFamily (i : Fin 3) : PlanarPacketFamily N κ ι :=
…
```
Mentions: OAI.LipschitzHilbert.PlanarPacketFamily
theorem OAI.LipschitzHilbert.SourceLatticePacket.rawJetFamily_derivative line 29

theorem OAI.LipschitzHilbert.SourceLatticePacket.rawJetFamily_reference_derivative line 46

Source documentation

The same exact horizontal normalization used for the zeroth jet.

theorem rawJetFamily_reference_derivative (i : Fin 3)
    (j : Fin N) (u : ι j) (k : κ) (y x : ℝ) :
    let Q := (P.rawJetFamily i).horizontalRescale P.topLength P.topLength_pos
…

def OAI.LipschitzHilbert.SourceLatticePacket.mixedReferenceJetLine line 70
theorem OAI.LipschitzHilbert.SourceLatticePacket.mixedReferenceJetLine_coeff line 82
theorem OAI.LipschitzHilbert.SourceLatticePacket.mixedReferenceJetLine_wave line 87
theorem OAI.LipschitzHilbert.SourceLatticePacket.mixedReferenceJetLine_budget_iff line 92
def OAI.LipschitzHilbert.SourceLatticePacket.mixedReferenceJetBand line 99
Source documentation
Actual unmasked synthesis with the original frozen analyzing coefficient and the requested covariant jet.
```
def mixedReferenceJetBand (i : Fin 3) (j : Fin N) (y x : ℝ) : EuclideanSpace ℂ κ :=
…
```
theorem OAI.LipschitzHilbert.SourceLatticePacket.mixedReferenceJetLine_partial line 104
theorem OAI.LipschitzHilbert.SourceLatticePacket.mixedReferenceJetBand_variation line 125

theorem OAI.LipschitzHilbert.SourceLatticePacket.mixed_reference_jet_uniform_moments line 143

Source documentation

The jet index changes neither the original analyzing budget nor the moment constant. Annuli are required for the actual jet waves.

theorem mixed_reference_jet_uniform_moments (hL : LepingleInput) {lo hi : ℝ}
    (hlo : 0 < lo) (hhi : 0 ≤ hi) :
    ∃ A M : ℝ, 0 < A ∧ 0 < M ∧ ∀ (N : ℕ) (κ : Type) (ι : Fin N → Type)
      [Fintype κ] [∀ j, Fintype (ι j)] (P : SourceLatticePacket N κ ι)
      (c : ∀ j, ι j → κ → ℂ) (hc : ∀ j u k, ‖c j u k‖ ≤ 1)
      (alt : ∀ j, ι j → κ → SchwartzMap (ℝ×ℝ) ℂ)
      (hAlt : ∀ j u k, planarProfileConstant (alt j u k) (2*P.order) ≤ P.profileBound)
      (d : Fin N → ℝ) (v : ℝ×ℝ → ℝ) (hv : Measurable v)
      (g : ℝ×ℝ → EuclideanSpace ℂ κ) (hg : Measurable g) (hg1 : ∀ z, ‖g z‖ ≤ 1),
      Monotone d →
      (∀ j u k y xi, |xi| < (lo/P.topLength)*(2:ℝ)^j.val →
        𝓕 ((P.frozenProfile c hc).raw 0 j u k y) xi = 0) →
…

Mentions: OAI.LipschitzHilbert.LepingleInput, OAI.LipschitzHilbert.SourceLatticePacket, OAI.LipschitzHilbert.planarProfileConstant, OAI.LipschitzHilbert.SourceLatticePacket.raw

theorem OAI.LipschitzHilbert.SourceLatticePacket.mixed_reference_jet_polynomial_tail line 203

Source documentation

The same fixed lower bound on L works for every jet, packet family, reference height and binary grid.

theorem mixed_reference_jet_polynomial_tail (hL : LepingleInput) {lo hi : ℝ}
    (hlo : 0 < lo) (hhi : 0 ≤ hi) (a J : ℝ) (ha : 0 ≤ a) (hJ : 0 ≤ J) :
    ∀ᶠ L : ℝ in Filter.atTop,
    ∀ (N : ℕ) (κ : Type) (ι : Fin N → Type)
      [Fintype κ] [∀ j, Fintype (ι j)] (P : SourceLatticePacket N κ ι),
      P.constant ≤ L^a →
    ∀ (c : ∀ j, ι j → κ → ℂ) (hc : ∀ j u k, ‖c j u k‖ ≤ 1)
      (alt : ∀ j, ι j → κ → SchwartzMap (ℝ×ℝ) ℂ)
      (hAlt : ∀ j u k, planarProfileConstant (alt j u k) (2*P.order) ≤ P.profileBound)
      (d : Fin N → ℝ) (v : ℝ×ℝ → ℝ) (hv : Measurable v)
      (g : ℝ×ℝ → EuclideanSpace ℂ κ) (hg : Measurable g) (hg1 : ∀ z, ‖g z‖ ≤ 1),
      Monotone d →
…

Mentions: OAI.LipschitzHilbert.LepingleInput, OAI.LipschitzHilbert.SourceLatticePacket, OAI.LipschitzHilbert.planarProfileConstant