OAI/Analysis/FactorGeneration/Correlation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Generator.exists_correlation_parameter line 12
2. theorem OAI.Generator.correlation_error_budget line 19

   Source documentation

   The strict nonlinear error budget in the manuscript, with its original constants.

   theorem correlation_error_budget {s α : ℝ} (hs : 0 < s) (hα : 0 < α)
       (hquarter : α < 1 / 4) (hsmall : α < s / 32) :
       s * (4 * α ^ 2 / (1 - 2 * α)) < α * s ^ 2 / 4 := by
   …

3. theorem OAI.Generator.correlation_lower_bound line 34

   Source documentation

   Triangle-inequality step converting the correlation error into a lower bound.

   theorem correlation_lower_bound {s α δ : ℝ} (hs : 0 < s) (hα : 0 < α)
       (hquarter : α < 1 / 4) (hsmall : α < s / 32) {c : ℂ}
       (hc : ‖c - ((α * s ^ 2 / 2 : ℝ) : ℂ)‖ ≤
         s * (4 * α ^ 2 / (1 - 2 * α)) + δ) :
       α * s ^ 2 / 4 - δ ≤ ‖c‖ := by
   …

4. theorem OAI.Generator.no_continuous_correlated_sequence line 48