OAI/Dynamics/TriangleBilliards/SpatialRigidity.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TriangularBilliards.smoothing_weak_limit line 45
2. def OAI.TriangularBilliards.clearanceCost line 55
3. lemma OAI.TriangularBilliards.clearanceCost_nonneg line 58
4. lemma OAI.TriangularBilliards.clearance_first_limit line 64

   Source documentation

   The genuine fixed-s weak limit. The ε-dependent mode energy is allowed to grow as s goes to zero; no s-independent bound is used at this stage.

   lemma clearance_first_limit (Q : Triangle) {H s : ℝ} (hH : 0 ≤ H) (hs : 0 < s)
       {f : DoubleL2 Q} (hf : ∀ᵐ z ∂doubleMeasure Q, ‖f z‖ ≤ H)
       (hinv : ∀ t, (geodesicHilbertFlow Q).act t f = f)
       (j : ℤ) {U B : DoubleL2 Q}
       (hUB : (geodesicHilbertFlow Q).HasGenerator U B)
       (hB : (angularCircleAction Q).projection (j-1) B = B) :
       ∃ g a b : DoubleL2 Q,
         (∀ᵐ z ∂doubleMeasure Q, ‖g z‖ ≤ H) ∧
         (geodesicHilbertFlow Q).HasGenerator g 0 ∧
         ‖g-f‖ ≤ H * (3*clearanceCost Q*s)^(1/2:ℝ) ∧
         RotationalCR (geodesicHilbertFlow Q) (transverseHilbertFlow Q) (angularCircleAction Q)
           ((angularCircleAction Q).projection j g) a b ∧ inner ℂ B b = 0 := by
   …

   Mentions: OAI.TriangularBilliards.Triangle, OAI.TriangularBilliards.DoubleL2, OAI.TriangularBilliards.doubleMeasure, OAI.TriangularBilliards.geodesicHilbertFlow, OAI.TriangularBilliards.angularCircleAction, OAI.TriangularBilliards.clearanceCost, OAI.TriangularBilliards.transverseHilbertFlow

5. lemma OAI.TriangularBilliards.Analysis.HilbertFlow.HasGenerator.invariant line 165
6. lemma OAI.TriangularBilliards.Analysis.HilbertFlow.hasGenerator_zero_iff line 172
7. lemma OAI.TriangularBilliards.Analysis.RotationalCR.unique_pair line 177
8. lemma OAI.TriangularBilliards.exists_bounded_representative line 190
9. lemma OAI.TriangularBilliards.bounded_invariant_CR_ae line 206
10. lemma OAI.TriangularBilliards.clearance_second_limit line 225

    Source documentation

    The second limit invokes the exact invariant uniform mode bound, not the fixed-s bound used before.

    lemma clearance_second_limit (Q : Triangle) {H : ℝ} (hH : 0 ≤ H)
        {f : DoubleL2 Q} (hf : ∀ᵐ z ∂doubleMeasure Q, ‖f z‖ ≤ H)
        (hinv : ∀ t, (geodesicHilbertFlow Q).act t f = f)
        (j : ℤ) {a b U : DoubleL2 Q}
        (hcr : RotationalCR (geodesicHilbertFlow Q) (transverseHilbertFlow Q)
          (angularCircleAction Q) ((angularCircleAction Q).projection j f) a b)
        (hUb : (geodesicHilbertFlow Q).HasGenerator U b) : b=0 := by
    …

    Mentions: OAI.TriangularBilliards.Triangle, OAI.TriangularBilliards.DoubleL2, OAI.TriangularBilliards.doubleMeasure, OAI.TriangularBilliards.geodesicHilbertFlow, OAI.TriangularBilliards.transverseHilbertFlow, OAI.TriangularBilliards.angularCircleAction

11. theorem OAI.TriangularBilliards.bounded_invariant_rigidity line 263

    Source documentation

    Analytic rigidity, on the actual double of every nondegenerate triangle. No irrational-angle assumption is needed for this stage.

    theorem bounded_invariant_rigidity (Q : Triangle) {H : ℝ} (hH : 0 ≤ H)
        {f : DoubleL2 Q} (hf : ∀ᵐ z ∂doubleMeasure Q, ‖f z‖ ≤ H)
        (hinv : ∀ t, (geodesicHilbertFlow Q).act t f = f) (j : ℤ) :
        RotationalCR (geodesicHilbertFlow Q) (transverseHilbertFlow Q)
          (angularCircleAction Q) ((angularCircleAction Q).projection j f) 0 0 := by
    …

    Mentions: OAI.TriangularBilliards.Triangle, OAI.TriangularBilliards.DoubleL2, OAI.TriangularBilliards.doubleMeasure, OAI.TriangularBilliards.geodesicHilbertFlow, OAI.TriangularBilliards.transverseHilbertFlow, OAI.TriangularBilliards.angularCircleAction