OAI/Dynamics/ThreeTorus/Averaging.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Real-frequency fast averaging on the compact slow circle.

  1. abbrev OAI.ThreeTorus.fastHaar line 24
  2. abbrev OAI.ThreeTorus.fastProduct line 25
  3. lemma OAI.ThreeTorus.fast_integral_character line 28
  4. lemma OAI.ThreeTorus.fast_integral_mFourier line 36
  5. def OAI.ThreeTorus.fastOrbit line 46
  6. lemma OAI.ThreeTorus.continuous_fastOrbit line 49
  7. lemma OAI.ThreeTorus.fast_integrable_diag line 53
  8. lemma OAI.ThreeTorus.fast_integrable_prod line 58
  9. lemma OAI.ThreeTorus.fast_mFourier_diagonal line 62
  10. lemma OAI.ThreeTorus.fast_mFourier_limit line 71
  11. lemma OAI.ThreeTorus.fast_polynomial_limit line 99
  12. lemma OAI.ThreeTorus.fast_average_diagonal_dist line 119
  13. lemma OAI.ThreeTorus.fast_average_product_dist line 128
  14. lemma OAI.ThreeTorus.fast_average_torus line 136

    Source documentation

    Fast averaging on the two-torus, uniform over any sequence of offsets. This is the compact quotient form of source Lemma fast-average.

    lemma fast_average_torus (F : C(UnitAddTorus (Fin 2),ℂ)) (beta : ℕ → UnitAddCircle) :
    Tendsto (fun n => ∫ z, F (fastOrbit n (beta n) z) ∂fastHaar)
      atTop (𝓝 (∫ z, F z ∂fastProduct)) := by
…

    Mentions: OAI.ThreeTorus.fastOrbit, OAI.ThreeTorus.fastHaar, OAI.ThreeTorus.fastProduct

  15. def OAI.ThreeTorus.compactRealTorus line 166

    Source documentation

    Rescale a compactly supported real frequency variable to one fundamental interval. Its endpoints vanish, so the quotient is genuinely continuous.

    def compactRealTorus (H : ℝ × UnitAddCircle → ℂ) (hH : Continuous H) (M : ℕ) :
    UnitAddCircle → C(UnitAddCircle,ℂ) :=
…

    Mentions: OAI.ThreeTorus.H

  16. lemma OAI.ThreeTorus.continuous_compactRealTorus line 171
  17. lemma OAI.ThreeTorus.compactRealTorus_coe line 183
  18. lemma OAI.ThreeTorus.compact_rescale_integral line 189
  19. lemma OAI.ThreeTorus.circle_fast_rescale line 207
  20. lemma OAI.ThreeTorus.compactRealTorus_integral line 220
  21. lemma OAI.ThreeTorus.compactRealTorus_marginal line 238
  22. lemma OAI.ThreeTorus.fast_average_real_compact line 259

    Source documentation

    Source fast averaging on the real frequency axis, for compactly supported continuous data and every sequence of circle offsets. The frequency parameter is the actual passage integer, not a synthetic independent variable.

    lemma fast_average_real_compact {H : ℝ × UnitAddCircle → ℂ} (hH : Continuous H)
    {M : ℕ} (hM : 0 < M) (hS : ∀ s y, (M:ℝ) ≤ |s| → H (s,y) = 0)
    (β : ℕ → UnitAddCircle) :
    Tendsto (fun n : ℕ => ∫ s, H (s,(((n:ℝ)*s:ℝ):UnitAddCircle)+β n)) atTop
      (𝓝 (∫ s, ∫ y, H (s,y) ∂AddCircle.haarAddCircle)) := by
…

    Mentions: OAI.ThreeTorus.H

  23. lemma OAI.ThreeTorus.fast_average_real_compact_real line 297