SourceTransversePacketEnergy.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Slice energy with the full transverse decay retained. This is the estimate required for a transverse polynomial of order 103; no horizontal polynomial or horizontal center restriction is introduced.

theorem OAI.LipschitzHilbert.lattice_slice_energy line 13

theorem OAI.LipschitzHilbert.transverse_lattice_slice_energy line 71

Source documentation

The fixed transverse polynomial is paid for by 207 powers of transverse packet decay; one power remains for integration.

theorem transverse_lattice_slice_energy {N : ℕ} {κ : Type*} {ι : Fin N → Type*}
    [Fintype κ] [∀ j, Fintype (ι j)]
    (c : ∀ j, ι j → EuclideanSpace ℂ κ) (f : ∀ j, ι j → κ → SchwartzMap ℝ ℂ)
    (X Z : ∀ j, ι j → ℝ) (site : ∀ j, ι j → ℤ×ℤ) (len : Fin N → ℝ)
    (a0 b0 b W y C : ℝ) (hW : 0<W) (hlen : ∀ j, 0<len j)
    (hinj : ∀ j, Function.Injective (site j))
    (hX : ∀ j i, X j i=a0+len j*(site j i).1)
    (hZ : ∀ j i, Z j i=b0+W*(site j i).2)
    (hcenter : ∀ j i, |Z j i-b|≤2*W)
    (hf : ∀ j i k x, ‖f j i k x‖≤C*
      (lineEnvelope (X j i) (len j) 1 x*lineEnvelope (Z j i) W 207 y)) :
    polynomialWeight b (2*W) 103 y^2*
…

Mentions: OAI.LipschitzHilbert.lineEnvelope, OAI.LipschitzHilbert.polynomialWeight