SpectralBounds.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem313.finite_spectral_tail line 12

Source documentation

A finite spectral tail is controlled by its first degree moment.

theorem finite_spectral_tail {ι : Type u} (s : Finset ι)
    (mass degree : ι → ℝ) (cutoff : ℝ) (hcutoff : 0 < cutoff)
    (hmass : ∀ i ∈ s, 0 ≤ mass i)
    (hdegree : ∀ i ∈ s, 0 ≤ degree i) :
    (∑ i ∈ s with cutoff < degree i, mass i) ≤
      (∑ i ∈ s, degree i * mass i) / cutoff := by
…

theorem OAI.Problem313.finite_spectral_split line 34

Source documentation

Splitting at a positive spectral cutoff gives a low-degree term and a tail.

theorem finite_spectral_split {ι : Type u} (s : Finset ι)
    (mass degree : ι → ℝ) (cutoff : ℝ) (hcutoff : 0 < cutoff)
    (hmass : ∀ i ∈ s, 0 ≤ mass i)
    (hdegree : ∀ i ∈ s, 0 ≤ degree i) :
    (∑ i ∈ s, mass i) ≤
      (∑ i ∈ s with degree i ≤ cutoff, mass i) +
      (∑ i ∈ s, degree i * mass i) / cutoff := by
…

theorem OAI.Problem313.variance_tail_bias_cancellation line 48

Source documentation

The bias cancels exactly in the tail term at the bias-dependent cutoff.

theorem variance_tail_bias_cancellation (sigma ell : ℝ)
    (hsigma : sigma ≠ 0) (hell : ell ≠ 0) :
    sigma ^ 2 / ((sigma * ell / 64) ^ 2 / 2) = 8192 / ell ^ 2 := by
…

theorem OAI.Problem313.variance_from_spectral_capture line 55

Source documentation

Assemble low-degree capture and the Dirichlet identity into a variance bound.

theorem variance_from_spectral_capture {ι : Type u} (s : Finset ι)
    (mass degree : ι → ℝ) (sigma ell influence lowConstant : ℝ)
    (hsigma : 0 < sigma) (hell : 0 < ell)
    (hmass : ∀ i ∈ s, 0 ≤ mass i)
    (hdegree : ∀ i ∈ s, 0 ≤ degree i)
    (hcapture : (∑ i ∈ s with degree i ≤ (sigma * ell / 64) ^ 2 / 2, mass i)
      ≤ lowConstant * influence)
    (hdirichlet : (∑ i ∈ s, degree i * mass i) = sigma ^ 2 * influence) :
    (∑ i ∈ s, mass i) ≤ (lowConstant + 8192 / ell ^ 2) * influence := by
…

theorem OAI.Problem313.variance_constant_assembly line 75

Source documentation

The two numerical terms fit inside the advertised universal constant.

theorem variance_constant_assembly (t ell lowConstant : ℝ)
    (ht : 0 < t) (hell : t / 3 ≤ ell)
    (hlow : lowConstant ≤ 256 / t ^ 2) :
    lowConstant + 8192 / ell ^ 2 ≤ (2 : ℝ) ^ 17 / t ^ 2 := by
…

theorem OAI.Problem313.variance_constant_assembly_budget line 92

Source documentation

A more flexible numerical budget, useful with coarse exponential estimates.

theorem variance_constant_assembly_budget (t ell lowConstant budget : ℝ)
    (ht : 0 < t) (hell : t / 3 ≤ ell)
    (hlow : lowConstant ≤ budget / t ^ 2)
    (hbudget : budget + 73728 ≤ (2 : ℝ) ^ 17) :
    lowConstant + 8192 / ell ^ 2 ≤ (2 : ℝ) ^ 17 / t ^ 2 := by
…

theorem OAI.Problem313.variance_small_log_assembly line 109

Source documentation

A small logarithm only needs the elementary Poincaré bound.

theorem variance_small_log_assembly (t variance influence : ℝ)
    (ht : 0 < t) (htsmall : t ≤ 16) (hinfluence : 0 ≤ influence)
    (hpoincare : variance ≤ influence / 4) :
    variance ≤ ((2 : ℝ) ^ 17 / t ^ 2) * influence := by
…

theorem OAI.Problem313.variance_large_log_assembly line 123

Source documentation

Final algebraic combination, leaving only the graph-specific spectral input.

theorem variance_large_log_assembly (t ell variance influence lowConstant : ℝ)
    (ht : 0 < t) (hell : t / 3 ≤ ell) (hinfluence : 0 ≤ influence)
    (hlow : lowConstant ≤ 256 / t ^ 2)
    (hvariance : variance ≤ (lowConstant + 8192 / ell ^ 2) * influence) :
    variance ≤ ((2 : ℝ) ^ 17 / t ^ 2) * influence :=
…

theorem OAI.Problem313.variance_from_fourier_capture line 132

Source documentation

The spectral variance bound for Fourier coefficients indexed by finite supports.

theorem variance_from_fourier_capture {ι : Type u} [Fintype ι] [DecidableEq ι]
    (coeff : Finset ι → ℝ) (variance sigma ell influence lowConstant : ℝ)
    (hsigma : 0 < sigma) (hell : 0 < ell)
    (hvariance : variance = ∑ S : Finset ι with S.Nonempty, coeff S ^ 2)
    (hdirichlet : (∑ S : Finset ι, (S.card : ℝ) * coeff S ^ 2) = sigma ^ 2 * influence)
    (hcapture : (∑ S : Finset ι with S.Nonempty ∧
        (S.card : ℝ) ≤ (sigma * ell / 64) ^ 2 / 2, coeff S ^ 2)
      ≤ lowConstant * influence) :
    variance ≤ (lowConstant + 8192 / ell ^ 2) * influence := by
…

theorem OAI.Problem313.variance_le_dirichlet_of_fourier line 158

Source documentation

Parseval and the first spectral moment immediately imply Poincaré.

theorem variance_le_dirichlet_of_fourier {ι : Type u} [Fintype ι] [DecidableEq ι]
    (coeff : Finset ι → ℝ) (variance dirichlet : ℝ)
    (hvariance : variance = ∑ S : Finset ι with S.Nonempty, coeff S ^ 2)
    (hdirichlet : (∑ S : Finset ι, (S.card : ℝ) * coeff S ^ 2) = dirichlet) :
    variance ≤ dirichlet := by
…