OAI/Dynamics/TriangleBilliards/CircleFourier.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

Strongly continuous unitary circle actions and their genuine Fourier projections. This supplies the angular Hilbert-space calculus, not a new assumption on a billiard-invariant field.

  1. structure OAI.TriangularBilliards.Analysis.CircleAction line 36
  2. lemma OAI.TriangularBilliards.Analysis.CircleAction.act_neg line 47
  3. lemma OAI.TriangularBilliards.Analysis.CircleAction.adjoint line 51
  4. lemma OAI.TriangularBilliards.Analysis.CircleAction.weighted_continuous line 56
  5. lemma OAI.TriangularBilliards.Analysis.CircleAction.weighted_integrable line 60
  6. lemma OAI.TriangularBilliards.Analysis.CircleAction.fourier_norm_apply line 65
  7. lemma OAI.TriangularBilliards.Analysis.CircleAction.coeff_norm_bound line 69
  8. def OAI.TriangularBilliards.Analysis.CircleAction.projection line 79
  9. lemma OAI.TriangularBilliards.Analysis.CircleAction.projection_apply line 93
  10. lemma OAI.TriangularBilliards.Analysis.CircleAction.projection_norm_le line 97
  11. lemma OAI.TriangularBilliards.Analysis.CircleAction.fourier_arg_add line 101
  12. lemma OAI.TriangularBilliards.Analysis.CircleAction.fourier_arg_neg line 106
  13. lemma OAI.TriangularBilliards.Analysis.CircleAction.fourier_neg_mul_self line 111
  14. lemma OAI.TriangularBilliards.Analysis.CircleAction.projection_eigen line 115
  15. lemma OAI.TriangularBilliards.Analysis.CircleAction.integral_inner_left line 130
  16. lemma OAI.TriangularBilliards.Analysis.CircleAction.projection_adjoint line 136
  17. lemma OAI.TriangularBilliards.Analysis.CircleAction.projection_of_eigen line 148
  18. lemma OAI.TriangularBilliards.Analysis.CircleAction.projection_mul line 162
  19. lemma OAI.TriangularBilliards.Analysis.CircleAction.projection_idem line 166
  20. lemma OAI.TriangularBilliards.Analysis.CircleAction.projection_orthogonal line 170
  21. def OAI.TriangularBilliards.Analysis.CircleAction.mode line 176

    Source documentation

    The closed Fourier eigenspace, presented as the fixed space of the proved bounded projection rather than an assumed orthogonal decomposition.

    def mode (j : ℤ) : Submodule ℂ H :=
…
  22. lemma OAI.TriangularBilliards.Analysis.CircleAction.mem_mode line 180
  23. lemma OAI.TriangularBilliards.Analysis.CircleAction.projection_mem_mode line 184
  24. lemma OAI.TriangularBilliards.Analysis.CircleAction.mode_orthogonal line 187
  25. lemma OAI.TriangularBilliards.Analysis.CircleAction.projection_norm_sum line 194
  26. lemma OAI.TriangularBilliards.Analysis.CircleAction.projection_inner_self line 198
  27. lemma OAI.TriangularBilliards.Analysis.CircleAction.bessel line 204
  28. lemma OAI.TriangularBilliards.Analysis.CircleAction.summable_norm_projection line 218
  29. lemma OAI.TriangularBilliards.Analysis.CircleAction.summable_projection line 221
  30. lemma OAI.TriangularBilliards.Analysis.CircleAction.scalar_coeff line 225
  31. lemma OAI.TriangularBilliards.Analysis.CircleAction.eq_zero_of_projections_zero line 233
  32. lemma OAI.TriangularBilliards.Analysis.CircleAction.projections_ext line 251
  33. lemma OAI.TriangularBilliards.Analysis.CircleAction.tsum_projection line 257
  34. lemma OAI.TriangularBilliards.Analysis.CircleAction.hasSum_projection line 266
  35. lemma OAI.TriangularBilliards.Analysis.CircleAction.projection_escape line 271

    Source documentation

    An injective sequence of modes escapes every fixed vector strongly.

    lemma projection_escape {φ : ℕ → ℤ} (hφ : Function.Injective φ) (u : H) :
    Tendsto (fun n => V.projection (φ n) u) atTop (𝓝 0) := by
…
  36. lemma OAI.TriangularBilliards.Analysis.CircleAction.bounded_modes_escape line 279

    Source documentation

    Uniformly bounded remainder fields of escaping modes converge weakly in the scalar inner-product sense. No norm convergence of the remainders is claimed or needed in the endpoint equation.

    lemma bounded_modes_escape {φ : ℕ → ℤ} (hφ : Function.Injective φ)
    (r : ℕ → H) {C : ℝ} (hC : ∀ n, ‖r n‖ ≤ C)
    (hr : ∀ n, V.projection (φ n) (r n) = r n) (u : H) :
    Tendsto (fun n => inner ℂ u (r n)) atTop (𝓝 0) := by
…
  37. lemma OAI.TriangularBilliards.Analysis.CircleAction.parity_index_injective line 291
  38. lemma OAI.TriangularBilliards.Analysis.CircleAction.parity_summable line 296
  39. def OAI.TriangularBilliards.Analysis.CircleAction.parityTail line 301

    Source documentation

    The genuine one-sided parity tail of the angular decomposition.

    def parityTail (m : ℤ) (u : H) : H := ∑' n : ℕ, V.projection (m + 2 * (n : ℤ)) u
  40. lemma OAI.TriangularBilliards.Analysis.CircleAction.parityTail_convergence line 303
  41. lemma OAI.TriangularBilliards.Analysis.CircleAction.parityTail_projection_inside line 308
  42. lemma OAI.TriangularBilliards.Analysis.CircleAction.parityTail_projection_outside line 318