OAI/Analysis/Littlewood/MinimizingFamily.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

A minimizing family with vanishing second error moment.

  1. def OAI.AsymptoticallyMinimalLittlewoodFiniteFlatness.boolSign line 20
  2. abbrev OAI.AsymptoticallyMinimalLittlewoodFiniteFlatness.μ line 22
  3. def OAI.AsymptoticallyMinimalLittlewoodFiniteFlatness.circlePolynomial line 24
  4. lemma OAI.AsymptoticallyMinimalLittlewoodFiniteFlatness.fourier_nat line 27
  5. lemma OAI.AsymptoticallyMinimalLittlewoodFiniteFlatness.circlePolynomial_apply line 34
  6. def OAI.AsymptoticallyMinimalLittlewoodFiniteFlatness.signVector line 42
  7. lemma OAI.AsymptoticallyMinimalLittlewoodFiniteFlatness.signVector_signing line 44
  8. lemma OAI.AsymptoticallyMinimalLittlewoodFiniteFlatness.signing_eq_signVector line 48
  9. lemma OAI.AsymptoticallyMinimalLittlewoodFiniteFlatness.exists_minimizing_signing line 55
  10. def OAI.AsymptoticallyMinimalLittlewoodFiniteFlatness.minimizingBits line 63
  11. def OAI.AsymptoticallyMinimalLittlewoodFiniteFlatness.chosenSigns line 64
  12. lemma OAI.AsymptoticallyMinimalLittlewoodFiniteFlatness.chosenSigns_signing line 66
  13. lemma OAI.AsymptoticallyMinimalLittlewoodFiniteFlatness.chosenSigns_minimal line 69
  14. lemma OAI.AsymptoticallyMinimalLittlewoodFiniteFlatness.chosenSigns_eventually_bound line 80
  15. lemma OAI.AsymptoticallyMinimalLittlewoodFiniteFlatness.circlePolynomial_energy line 95

    Source documentation

    Exact finite Parseval, obtained from finite orthonormal Fourier sums.

    lemma circlePolynomial_energy {N : ℕ} (ε : Fin N → ℝ) :
    (∫ t : UnitAddCircle, ‖circlePolynomial ε t‖ ^ 2 ∂μ) = ∑ k, (ε k) ^ 2 := by
…

    Mentions: OAI.AsymptoticallyMinimalLittlewoodFiniteFlatness.circlePolynomial, OAI.AsymptoticallyMinimalLittlewoodFiniteFlatness.μ

  16. lemma OAI.AsymptoticallyMinimalLittlewoodFiniteFlatness.signing_energy line 118
  17. def OAI.AsymptoticallyMinimalLittlewoodFiniteFlatness.normalized line 126
  18. lemma OAI.AsymptoticallyMinimalLittlewoodFiniteFlatness.normalized_nonneg line 129
  19. lemma OAI.AsymptoticallyMinimalLittlewoodFiniteFlatness.normalized_continuous line 132
  20. lemma OAI.AsymptoticallyMinimalLittlewoodFiniteFlatness.normalized_measurable line 135
  21. lemma OAI.AsymptoticallyMinimalLittlewoodFiniteFlatness.normalized_eventually_bound line 139
  22. lemma OAI.AsymptoticallyMinimalLittlewoodFiniteFlatness.normalized_eventually_le_two line 147
  23. lemma OAI.AsymptoticallyMinimalLittlewoodFiniteFlatness.normalized_energy line 152
  24. lemma OAI.AsymptoticallyMinimalLittlewoodFiniteFlatness.continuous_integrable line 159
  25. lemma OAI.AsymptoticallyMinimalLittlewoodFiniteFlatness.normalized_error_sq_bound line 163

    Source documentation

    Elementary second-error-moment estimate; no p-dependent signing is used.

    lemma normalized_error_sq_bound {N : ℕ} (hN : 1 ≤ N) {η : ℝ} (hη : 0 < η)
    (hb : ∀ t, normalized N t ≤ 1 + η) :
    (∫ t : UnitAddCircle, (normalized N t - 1) ^ 2 ∂μ) ≤ 2 * η := by
…

    Mentions: OAI.AsymptoticallyMinimalLittlewoodFiniteFlatness.normalized, OAI.AsymptoticallyMinimalLittlewoodFiniteFlatness.μ

  26. lemma OAI.AsymptoticallyMinimalLittlewoodFiniteFlatness.normalized_error_sq_tendsto line 203