OAI/Dynamics/TriangleBilliards/SpatialConstancy.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TriangularBilliards.bounded_invariant_transverse line 43
2. lemma OAI.TriangularBilliards.transverse_invariant_smoothing_pairing_zero line 62
3. lemma OAI.TriangularBilliards.transverse_invariant_smoothing_zero line 77
4. lemma OAI.TriangularBilliards.realLinear_zero_of_velocity_transverse line 125
5. lemma OAI.TriangularBilliards.invariant_smoothing_gradient_zero line 144
6. lemma OAI.TriangularBilliards.double_ae_slices line 171
7. lemma OAI.TriangularBilliards.double_ae_of_slices line 181
8. lemma OAI.TriangularBilliards.smoothing_gradient_zero_on_slice line 194
9. lemma OAI.eventual_equal_of_vanishing_gradient line 219
10. lemma OAI.ae_constant_of_eventual_equal line 243
11. theorem OAI.TriangularBilliards.bounded_invariant_spatial_constancy line 265

    Source documentation

    The actual bounded invariant is independent of the spatial position on each of the two triangle sheets, almost everywhere in direction and sheet.

    theorem bounded_invariant_spatial_constancy (Q : Triangle)
        {f : DoublePhase → ℂ} (hfm : StronglyMeasurable f) (hf : MemLp f 2 (doubleMeasure Q))
        {H : ℝ} (hb : ∀ z, ‖f z‖ ≤ H)
        (hfx : (geodesicHilbertFlow Q).HasGenerator (hf.toLp f) 0) :
        ∀ᵐ c ∂angularMeasure.prod parityMeasure,
          (fun x => f ((x,c.1),c.2)) =ᵐ[(volume Q.table)⁻¹ • volume.restrict Q.table]
            (fun _ => ∫ x, f ((x,c.1),c.2) ∂((volume Q.table)⁻¹ • volume.restrict Q.table)) := by
    …

    Mentions: OAI.TriangularBilliards.Triangle, OAI.TriangularBilliards.DoublePhase, OAI.TriangularBilliards.doubleMeasure, OAI.TriangularBilliards.geodesicHilbertFlow, OAI.TriangularBilliards.parityMeasure