VarianceReduction.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem313.variance_bound_of_fourier_capture line 15

Source documentation

The graph-independent final step of the variance proof: capture at squared logarithmic degree, together with Parseval and the Dirichlet identity, yields the exact advertised numerical constant.

theorem variance_bound_of_fourier_capture {ι : Type u} [Fintype ι] [DecidableEq ι]
    (coeff : Finset ι → ℝ) (variance sigma influence t m : ℝ)
    (hsigma : 0 < sigma) (hinfluence : 0 ≤ influence)
    (ht : 0 < t) (hm : 0 < m) (hlog : t / 3 ≤ Real.log m)
    (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 * Real.log m / 64) ^ 2 / 2, coeff S ^ 2)
      ≤ (4 * m ^ (-1 / 4 : ℝ)) * influence) :
    variance ≤ ((2 : ℝ) ^ 17 / t ^ 2) * influence := by
…

theorem OAI.Problem313.variance_bound_of_fourier_inputs line 37

Source documentation

A complete numerical reduction for all logarithmic scales. The only large-scale input remaining is capture of low Fourier supports.

theorem variance_bound_of_fourier_inputs {ι : Type u} [Fintype ι] [DecidableEq ι]
    (coeff : Finset ι → ℝ) (variance sigma influence t : ℝ)
    (hsigma : 0 < sigma) (hsigma_sq : sigma ^ 2 ≤ 1 / 4)
    (hinfluence : 0 ≤ influence) (ht : 0 < t)
    (hvariance : variance = ∑ S : Finset ι with S.Nonempty, coeff S ^ 2)
    (hdirichlet : (∑ S : Finset ι, (S.card : ℝ) * coeff S ^ 2) = sigma ^ 2 * influence)
    (hcapture : 16 ≤ t → ∃ m : ℝ, 0 < m ∧ t / 3 ≤ Real.log m ∧
      (∑ S : Finset ι with S.Nonempty ∧
        (S.card : ℝ) ≤ (sigma * Real.log m / 64) ^ 2 / 2, coeff S ^ 2)
        ≤ (4 * m ^ (-1 / 4 : ℝ)) * influence) :
    variance ≤ ((2 : ℝ) ^ 17 / t ^ 2) * influence := by
…