SourcePhaseNorm.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Coordinate bounds on the actual shift simplex, and the polynomial budget for the linear node envelope at arbitrary imaginary phases.

theorem OAI.LipschitzHilbert.sourceShiftSimplex_phase_norm line 14
theorem OAI.LipschitzHilbert.sourceShiftSimplex_phase_re line 33

theorem OAI.LipschitzHilbert.eventually_source_linear_phase_budget line 42

Source documentation

The explicit node-envelope coefficient grows at most linearly in the imaginary norm; its remaining factors are fixed powers of L.

theorem eventually_source_linear_phase_budget (C q : ℝ) (hC : 1 ≤ C) :
    ∀ᶠ L : ℝ in atTop, ∀ (a Z A r H : ℝ) (K : ℕ),
      0 ≤ a → a ≤ 1 → 0 ≤ Z → 0 ≤ r → Z ≤ 1+r →
      0 ≤ A → A ≤ L^q → (K:ℝ) ≤ L^2 → 0 ≤ H → H ≤ 3*L →
      C^8*A*(1+(a+Z*K)*(H+1))*C^3 ≤ L^(q+4)*(1+r) := by
…