OAI/Dynamics/TriangleBilliards/Main.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TriangularBilliards.spatialMean line 47
2. lemma OAI.TriangularBilliards.spatialMean_stronglyMeasurable line 50
3. lemma OAI.TriangularBilliards.Triangle.clearance_pos_of_mem_side line 56
4. lemma OAI.TriangularBilliards.Triangle.side_mem_hull line 64
5. lemma OAI.TriangularBilliards.directS_eq_const_of_slice line 70
6. lemma OAI.TriangularBilliards.reflectedSmoothing_eq_const_of_slice line 98
7. lemma OAI.equal_of_zero_gradient_openSegment line 115
8. lemma OAI.irrational_arg_of_angle line 125
9. lemma OAI.complex_div_conj_eq_exp_double_arg line 135
10. lemma OAI.TriangularBilliards.spatialMean_reflection_invariant line 152
11. lemma OAI.TriangularBilliards.reflectedDirection_pair line 232
12. lemma OAI.TriangularBilliards.angle_irrational_ergodic line 261
13. lemma OAI.TriangularBilliards.angular_reflections_constant line 271
14. lemma OAI.ae_fst_of_ae_prod line 306
15. lemma OAI.measure_zero_or_one_of_indicator_constant line 313
16. lemma OAI.invariant_indicator line 338
17. theorem OAI.TriangularBilliards.bounded_billiard_invariant_constant line 357

    Source documentation

    Every bounded measurable invariant of the actual billiard is constant. Spatial rigidity is proved above on the oriented double; side holonomy now uses the actual irrational angle, with no Diophantine rate assumption.

    theorem bounded_billiard_invariant_constant (Q : Triangle) (hQ : Q.HasIrrationalAngle)
        {f : Phase → ℂ} (hfm : StronglyMeasurable f) (hf : MemLp f 2 (phaseMeasure Q))
        {H : ℝ} (hb : ∀ z, ‖f z‖ ≤ H)
        (hinv : ∀ t : ℝ, (fun z => f (billiardFlow Q t z)) =ᵐ[phaseMeasure Q] f) :
        ∃ c : ℂ, f =ᵐ[phaseMeasure Q] fun _ => c := by
    …

    Mentions: OAI.TriangularBilliards.Triangle, OAI.TriangularBilliards.Phase, OAI.TriangularBilliards.phaseMeasure, OAI.TriangularBilliards.billiardFlow

18. theorem OAI.TriangularBilliards.irrational_triangle_invariant_set line 402

    Source documentation

    The invariant-set endpoint, for invariance modulo null sets at every real (time), on the normalized interior phase space of every irrational triangle.

    theorem irrational_triangle_invariant_set (Q : Triangle) (hQ : Q.HasIrrationalAngle)
        (A : Set Phase) (hA : MeasurableSet A)
        (hAi : ∀ t : ℝ, phaseMeasure Q (((billiardFlow Q t) ⁻¹' A) ∆ A)=0) :
        phaseMeasure Q A=0 ∨ phaseMeasure Q A=1 := by
    …

    Mentions: OAI.TriangularBilliards.Triangle, OAI.TriangularBilliards.Phase, OAI.TriangularBilliards.phaseMeasure, OAI.TriangularBilliards.billiardFlow

19. theorem OAI.TriangularBilliards.irrational_triangle_billiard line 418

    Source documentation

    Full two-sided billiard ergodicity, including complete regular chains and the geometric and measure-theoretic guarantees.

    Distinct definitions of this name: ComparatorChallenges/IrrationalTriangleBilliard.lean:119 (same statement text; different proof or body). Qualify references as OAI.TriangularBilliards.irrational_triangle_billiard@path.

    theorem irrational_triangle_billiard (Q : Triangle) (hQ : Q.HasIrrationalAngle) :
        MainConclusion Q := by
    …

    Mentions: OAI.TriangularBilliards.Triangle, OAI.TriangularBilliards.MainConclusion

20. theorem OAI.TriangularBilliards.irrational_triangle_nullMeasurable_set line 427

    Source documentation

    The same conclusion for the completion of the area-angular measure. Thus "measurable" may also be read in the Lebesgue-completed sense.

    theorem irrational_triangle_nullMeasurable_set (Q : Triangle) (hQ : Q.HasIrrationalAngle)
        (A : Set Phase) (hA : NullMeasurableSet A (phaseMeasure Q))
        (hAi : ∀ t : ℝ, phaseMeasure Q (((billiardFlow Q t) ⁻¹' A) ∆ A)=0) :
        phaseMeasure Q A=0 ∨ phaseMeasure Q A=1 := by
    …

    Mentions: OAI.TriangularBilliards.Triangle, OAI.TriangularBilliards.Phase, OAI.TriangularBilliards.phaseMeasure, OAI.TriangularBilliards.billiardFlow