OAI/Dynamics/ThreeTorus/BlockMoments.lean

GitHub source file

91 declarations, 0 contain sorry, 0 declared as axioms

Finite-color moment laws, binomial estimates, and phase expansion.

  1. lemma OAI.ThreeTorus.binomial_quadratic_remainder line 12
  2. lemma OAI.ThreeTorus.binomial_exponential_remainder line 41
  3. abbrev OAI.ThreeTorus.phaseHaar line 60
  4. abbrev OAI.ThreeTorus.phaseProduct line 61
  5. lemma OAI.ThreeTorus.integrable_circle line 64
  6. def OAI.ThreeTorus.blockFactor line 68
  7. def OAI.ThreeTorus.blockFactorC line 71
  8. lemma OAI.ThreeTorus.blockFactor_cast line 74
  9. lemma OAI.ThreeTorus.continuous_blockFactor line 79
  10. lemma OAI.ThreeTorus.continuous_blockFactorC line 83
  11. lemma OAI.ThreeTorus.blockFactor_bounds line 87
  12. lemma OAI.ThreeTorus.integral_phase_character line 96
  13. lemma OAI.ThreeTorus.integral_character_blockFactorC line 104
  14. lemma OAI.ThreeTorus.integral_blockFactorC line 120
  15. lemma OAI.ThreeTorus.integral_blockFactor line 124
  16. lemma OAI.ThreeTorus.integral_blockFactorC_mul line 131
  17. lemma OAI.ThreeTorus.integral_blockFactor_mul line 148
  18. def OAI.ThreeTorus.blockProduct line 157
  19. lemma OAI.ThreeTorus.integral_blockProduct line 160
  20. lemma OAI.ThreeTorus.integral_blockProduct_mul line 166
  21. lemma OAI.ThreeTorus.blockProduct_nonneg line 174
  22. lemma OAI.ThreeTorus.square_root_polynomial_bound line 180
  23. lemma OAI.ThreeTorus.continuous_blockProduct line 186
  24. lemma OAI.ThreeTorus.integrable_phaseProduct line 191
  25. def OAI.ThreeTorus.blockMixture line 195
  26. lemma OAI.ThreeTorus.continuous_blockMixture line 198
  27. lemma OAI.ThreeTorus.integral_blockMixture line 205
  28. lemma OAI.ThreeTorus.integral_blockMixture_sq line 213
  29. lemma OAI.ThreeTorus.integral_blockMixture_variance line 239
  30. lemma OAI.ThreeTorus.blockMixture_nonneg line 254
  31. lemma OAI.ThreeTorus.weighted_complex_cross line 265
  32. lemma OAI.ThreeTorus.block_pair_bound line 278
  33. lemma OAI.ThreeTorus.blockMixture_variance_bound line 300
  34. lemma OAI.ThreeTorus.blockMixture_hellinger_bound line 327
  35. lemma OAI.ThreeTorus.block_hellinger_numerical_constant line 357
  36. def OAI.ThreeTorus.weightedProduct line 379

    Source documentation

    Tensor density on an n-fold product probability space.

    def weightedProduct (h : X → ℝ) (n : ℕ) (z : Fin n → X) : ℝ := ∏ i, h (z i)
  37. lemma OAI.ThreeTorus.weightedProduct_one_factor line 381
  38. lemma OAI.ThreeTorus.weightedProduct_two_centered line 398
  39. lemma OAI.ThreeTorus.continuous_weightedProduct line 421
  40. lemma OAI.ThreeTorus.integral_weightedProduct_centered_sum line 426
  41. lemma OAI.ThreeTorus.integral_weightedProduct_centered_sq line 439
  42. lemma OAI.ThreeTorus.integral_weighted_norm_sub_sq line 482
  43. lemma OAI.ThreeTorus.integral_block_centered line 507
  44. lemma OAI.ThreeTorus.integral_block_centered_sq line 518
  45. lemma OAI.ThreeTorus.integral_block_sum_centered line 531
  46. lemma OAI.ThreeTorus.integral_block_sum_centered_sq line 539
  47. def OAI.ThreeTorus.blockEstimatorNoise line 549
  48. lemma OAI.ThreeTorus.continuous_blockEstimatorNoise line 552
  49. lemma OAI.ThreeTorus.integral_blockEstimatorNoise line 557
  50. lemma OAI.ThreeTorus.integral_blockEstimatorNoise_sq line 563
  51. lemma OAI.ThreeTorus.integral_weighted_norm_add_centered line 574
  52. lemma OAI.ThreeTorus.block_estimator_previous_error line 597
  53. lemma OAI.ThreeTorus.block_estimator_variance_bound line 606
  54. lemma OAI.ThreeTorus.circle_fourierCoeff_realIntegral line 622
  55. lemma OAI.ThreeTorus.circle_fourierCoeff_tendsto line 639
  56. lemma OAI.ThreeTorus.separated_frequency_large line 647

    Source documentation

    A quantitative last-nonzero-frequency estimate. It admits an arbitrary additional lower bound at each successive choice of L.

    lemma separated_frequency_large {n : ℕ} {R D : ℤ} {L ν : Fin n → ℤ}
    (hL : ∀ i, 0 ≤ L i) (hν : ν ≠ 0) (hD : ∀ i, |ν i| ≤ D)
    (hgap : ∀ j, R + D * ∑ i ∈ Finset.univ.filter (· < j), L i < L j) :
    R < |∑ i, ν i * L i| := by
…
  57. lemma OAI.ThreeTorus.finite_fourierCoeff_bound line 699

    Source documentation

    Uniform Riemann--Lebesgue bounds for a finite coefficient list.

    lemma finite_fourierCoeff_bound {ι : Type*} [Finite ι] (c : ι → UnitAddCircle → ℂ)
    {ε : ℝ} (hε : 0 < ε) :
    ∃ R : ℤ, 0 ≤ R ∧ ∀ k : ℤ, R < |k| → ∀ i, ‖fourierCoeff (c i) k‖ < ε := by
…
  58. lemma OAI.ThreeTorus.phase_integral_mFourier line 720
  59. lemma OAI.ThreeTorus.mFourier_diagonal line 730
  60. def OAI.ThreeTorus.phaseTest line 745

    Source documentation

    A finite Laurent expression, with coefficients depending measurably on its original circle variable.

    def phaseTest {ι : Type*} [Fintype ι] {n : ℕ}
    (c : ι → UnitAddCircle → ℂ) (ν : ι → Fin n → ℤ)
    (z : UnitAddCircle) (y : UnitAddTorus (Fin n)) : ℂ :=
…
  61. lemma OAI.ThreeTorus.integral_phaseTest_independent line 750
  62. lemma OAI.ThreeTorus.integral_phaseTest_diagonal line 777
  63. lemma OAI.ThreeTorus.finite_phase_test_bounds line 794

    Source documentation

    All of a finite family of phase tests are accurate for every sufficiently separated positive frequency tuple. Thus the gaps can be strengthened during a geometric construction without invalidating earlier tests.

    lemma finite_phase_test_bounds {κ ι : Type*} [Fintype κ] [Fintype ι] {n : ℕ}
    (c : κ → ι → UnitAddCircle → ℂ) (ν : κ → ι → Fin n → ℤ)
    (hc : ∀ k i, Integrable (c k i) phaseHaar) {ε : ℝ} (hε : 0 < ε) :
    ∃ R D : ℤ, 0 ≤ R ∧ 0 ≤ D ∧ ∀ L : Fin n → ℤ,
      (∀ i, 0 ≤ L i) →
      (∀ j, R + D * ∑ i ∈ Finset.univ.filter (· < j), L i < L j) →
      ∀ k, ‖(∫ z, phaseTest (c k) (ν k) z (fun i => L i • z) ∂phaseHaar) -
        (∫ z, ∫ y, phaseTest (c k) (ν k) z y ∂volume ∂phaseHaar)‖ < ε := by
…

    Mentions: OAI.ThreeTorus.phaseHaar, OAI.ThreeTorus.phaseTest

  64. def OAI.ThreeTorus.phaseFrequencies line 838

    Source documentation

    The recursive choices allow any finite lower bound depending on the already selected frequencies.

    def phaseFrequencies (R D : ℤ) (B : (j : ℕ) → (Fin j → ℤ) → ℤ) : ℕ → ℤ :=
…
  65. lemma OAI.ThreeTorus.phaseFrequencies_eq line 843
  66. lemma OAI.ThreeTorus.sum_fin_lt_eq_prefix line 850
  67. lemma OAI.ThreeTorus.phaseFrequencies_pos line 866
  68. lemma OAI.ThreeTorus.phaseFrequencies_lower line 874
  69. lemma OAI.ThreeTorus.phaseFrequencies_gap line 881
  70. theorem OAI.ThreeTorus.finite_phase_tests line 892

    Source documentation

    Source Lemma phase-tests, including arbitrary lower bounds at each successive frequency choice.

    theorem finite_phase_tests {κ ι : Type*} [Fintype κ] [Fintype ι] {n : ℕ}
    (c : κ → ι → UnitAddCircle → ℂ) (ν : κ → ι → Fin n → ℤ)
    (hc : ∀ k i, Integrable (c k i) phaseHaar) {ε : ℝ} (hε : 0 < ε)
    (B : (j : ℕ) → (Fin j → ℤ) → ℤ) :
    ∃ L : Fin n → ℤ, (∀ j, 0 < L j) ∧
      (∀ j : Fin n, B j (fun i => L ⟨i.val, i.isLt.trans j.isLt⟩) < L j) ∧
      ∀ k, ‖(∫ z, phaseTest (c k) (ν k) z (fun i => L i • z) ∂phaseHaar) -
        (∫ z, ∫ y, phaseTest (c k) (ν k) z y ∂volume ∂phaseHaar)‖ < ε := by
…

    Mentions: OAI.ThreeTorus.phaseHaar, OAI.ThreeTorus.phaseTest

  71. def OAI.ThreeTorus.CircleBounded line 926

    Source documentation

    A bounded measurable coefficient on the temporal circle.

    def CircleBounded (f : UnitAddCircle → ℂ) : Prop :=
…
  72. lemma OAI.ThreeTorus.CircleBounded.integrable line 929
  73. lemma OAI.ThreeTorus.CircleBounded.const line 934
  74. lemma OAI.ThreeTorus.CircleBounded.add line 937
  75. lemma OAI.ThreeTorus.CircleBounded.mul line 944
  76. lemma OAI.ThreeTorus.CircleBounded.conj line 952
  77. lemma OAI.ThreeTorus.CircleBounded.continuous line 957
  78. def OAI.ThreeTorus.PhaseLaurent line 965

    Source documentation

    An actual finite expansion; every coefficient is proved measurable and bounded. The finite coefficient type can vary with the expression.

    def PhaseLaurent {n : ℕ} (F : UnitAddCircle → (Fin n → UnitAddCircle) → ℂ) : Prop :=
…
  79. lemma OAI.ThreeTorus.PhaseLaurent.coeff line 970
  80. lemma OAI.ThreeTorus.PhaseLaurent.character line 976
  81. lemma OAI.ThreeTorus.PhaseLaurent.add line 982
  82. lemma OAI.ThreeTorus.PhaseLaurent.mul line 998
  83. lemma OAI.ThreeTorus.PhaseLaurent.conj line 1018
  84. lemma OAI.ThreeTorus.PhaseLaurent.neg line 1029
  85. lemma OAI.ThreeTorus.PhaseLaurent.sub line 1033
  86. lemma OAI.ThreeTorus.PhaseLaurent.sum line 1037
  87. lemma OAI.ThreeTorus.PhaseLaurent.prod line 1048
  88. lemma OAI.ThreeTorus.PhaseLaurent.norm_sq line 1059
  89. lemma OAI.ThreeTorus.PhaseLaurent.bounds line 1067
  90. lemma OAI.ThreeTorus.PhaseLaurent.finite_bounds line 1082
  91. theorem OAI.ThreeTorus.PhaseLaurent.finite_tests line 1106

    Source documentation

    Compatible averaging for any finite collection of expressions assembled from the actual fixed pre-block data, with all forward construction bounds.

    theorem PhaseLaurent.finite_tests {κ : Type*} [Fintype κ] {n : ℕ}
    {F : κ → UnitAddCircle → (Fin n → UnitAddCircle) → ℂ}
    (hF : ∀ k, PhaseLaurent (F k)) {ε : ℝ} (hε : 0 < ε)
    (B : (j : ℕ) → (Fin j → ℤ) → ℤ) :
    ∃ L : Fin n → ℤ, (∀ j, 0 < L j) ∧
      (∀ j : Fin n, B j (fun i => L ⟨i.val, i.isLt.trans j.isLt⟩) < L j) ∧
      ∀ k, ‖(∫ z, F k z (fun i => L i • z) ∂phaseHaar) -
        (∫ z, ∫ y, F k z y ∂phaseProduct n ∂phaseHaar)‖ < ε := by
…

    Mentions: OAI.ThreeTorus.PhaseLaurent, OAI.ThreeTorus.phaseHaar, OAI.ThreeTorus.phaseProduct