SourceMaskedAmplitude.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Original length restrictions and the common top mask in the actual source analytic amplitude. Small masks retain their full gain when the single-top bounds are summed over an eligible angular node.

theorem OAI.LipschitzHilbert.AngularGrid.sourcePacketAmplitude_smul_value line 18

theorem OAI.LipschitzHilbert.AngularGrid.sourcePacketAmplitude_masked_restricted_envelope line 38

Source documentation

The bound uses the original analyzing coefficients and their interval concentration, even after any interval of original lengths is retained.

theorem sourcePacketAmplitude_masked_restricted_envelope
    (grid : AngularGrid) (tops : Finset ι)
    (slope precision : ι → ℝ) (cutoff : ℝ) (weight : ι → X → ℝ)
    (hp : ∀ i ∈ tops, 0 ≤ precision i) (hw : ∀ i z, 0 < weight i z)
    {K : ℕ} (hK : 0 < K) (gap : ℕ → ℝ) (phase : ℕ → ℂ)
    (M : ℕ) (top : ι) (htop : top ∈ tops)
    (he : grid.eligible cutoff (precision top) M) (z : X)
    (a Z : ℝ) (ha0 : 0 ≤ a) (ha1 : a ≤ 1) (hZ : 0 ≤ Z)
    (hz0 : ∀ j < M, 0 ≤ (phase j).re) (hz : ∀ j < M, ‖phase j‖ ≤ Z)
    {N : ℕ} {κ : Type} {Label : Fin N → Type} {Item : ∀ j, Label j → Type}
    [Fintype κ] [∀ j l, Fintype (Item j l)]
    (P : SourceLabeledLattice N κ Label Item)
…

Mentions: OAI.LipschitzHilbert.AngularGrid, OAI.LipschitzHilbert.SourceLabeledLattice

theorem OAI.LipschitzHilbert.AngularGrid.node_masked_amplitude_envelope line 77

Source documentation

In particular the exponential smallness of every insignificant top mask survives the sum, with no loss proportional to the number of tops.

theorem node_masked_amplitude_envelope {E : Type*} [NormedAddCommGroup E]
    [NormedSpace ℂ E] (grid : AngularGrid) (tops : Finset ι)
    (slope precision : ι → ℝ) (cutoff : ℝ) (weight : ι → X → ℝ)
    (amplitude : ι → E) (q : ι → ℂ) (level : ℕ) (cell : ℤ) (z : X)
    (A C ε : ℝ) (hA : 0 ≤ A) (hε : 0 ≤ ε)
    (hw : ∀ i ∈ grid.cellTops tops slope precision cutoff level cell, 0 ≤ weight i z)
    (hC : ∀ i ∈ grid.cellTops tops slope precision cutoff level cell, weight i z ≤ C)
    (hq : ∀ i ∈ grid.cellTops tops slope precision cutoff level cell, ‖q i‖ ≤ ε)
    (hamp : ∀ i ∈ grid.cellTops tops slope precision cutoff level cell,
      ‖amplitude i‖ ≤ A*(weight i z)^4) :
    ‖∑ i ∈ grid.cellTops tops slope precision cutoff level cell, q i • amplitude i‖ ≤
      (A*C^3)*ε*grid.mass tops slope precision cutoff weight level cell z := by
…

Mentions: OAI.LipschitzHilbert.AngularGrid