LowDegreeL4.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem313.inverse_noise_energy_le line 15

Source documentation

Removing a diagonal noise multiplier costs at most rho ^ (-2*k) in squared coefficient norm on coefficients supported in degrees at most k.

theorem inverse_noise_energy_le {ι : Type u} [Fintype ι]
    (degree : ι → ℕ) (c : ι → ℝ) (rho k : ℝ)
    (hrho : 0 < rho) (hrho1 : rho ≤ 1)
    (hdegree : ∀ i, c i ≠ 0 → (degree i : ℝ) ≤ k) :
    (∑ i, (rho ^ (-(degree i : ℝ)) * c i) ^ 2) ≤
      rho ^ (-2 * k) * ∑ i, (c i) ^ 2 := by
…

theorem OAI.Problem313.lowDegree_fourth_of_noise line 38

Source documentation

Spectral inversion turns a diagonal-noise L² → L⁴ estimate into an L⁴ estimate for a low-degree expansion. This version is independent of any particular construction of the orthonormal basis.

theorem lowDegree_fourth_of_noise
    {ι : Type u} {X : Type v} [Fintype ι] [Fintype X]
    (degree : ι → ℕ) (basis : ι → X → ℝ) (weight : X → ℝ)
    (rho k : ℝ) (hrho : 0 < rho) (hrho1 : rho ≤ 1)
    (hnoise : ∀ a : ι → ℝ,
      (∑ x, weight x * (∑ i, rho ^ (degree i : ℝ) * a i * basis i x) ^ 4) ≤
        (∑ i, (a i) ^ 2) ^ 2)
    (c : ι → ℝ) (hdegree : ∀ i, c i ≠ 0 → (degree i : ℝ) ≤ k) :
    (∑ x, weight x * (∑ i, c i * basis i x) ^ 4) ≤
      rho ^ (-4 * k) * (∑ i, (c i) ^ 2) ^ 2 := by
…