OAI/Dynamics/TriangleBilliards/MeasurableFlow.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

Borel realization of full chains. Countable collision data, rather than an uncountable trajectory selector, permit a standard-Borel inverse.

  1. lemma OAI.TriangularBilliards.Triangle.side_coords_nonneg line 18
  2. lemma OAI.TriangularBilliards.Triangle.measurableSet_side line 27
  3. lemma OAI.TriangularBilliards.Triangle.inside_of_midpoint line 36
  4. abbrev OAI.TriangularBilliards.ChainData line 57
  5. def OAI.TriangularBilliards.ChainData.time line 61
  6. def OAI.TriangularBilliards.ChainData.point line 62
  7. def OAI.TriangularBilliards.ChainData.direction line 63
  8. def OAI.TriangularBilliards.ChainData.wall line 64
  9. def OAI.TriangularBilliards.ChainData.Valid line 68

    Source documentation

    Every predicate is a countable combination of Borel coordinate predicates. Midpoint membership entails the entire open-flight condition by convexity.

    def Valid (Q : Triangle) (z : Phase) (c : ChainData) : Prop :=
…

    Mentions: OAI.TriangularBilliards.Triangle, OAI.TriangularBilliards.Phase, OAI.TriangularBilliards.ChainData

  10. def OAI.TriangularBilliards.ChainData.toChain line 83
  11. def OAI.TriangularBilliards.FlightChain.data line 114
  12. lemma OAI.TriangularBilliards.FlightChain.data_valid line 117
  13. lemma OAI.TriangularBilliards.ChainData.continuous_time line 129
  14. lemma OAI.TriangularBilliards.ChainData.continuous_point line 133
  15. lemma OAI.TriangularBilliards.ChainData.continuous_direction line 137
  16. lemma OAI.TriangularBilliards.ChainData.continuous_wall line 141
  17. lemma OAI.TriangularBilliards.ChainData.measurableSet_side_mem line 145
  18. lemma OAI.TriangularBilliards.ChainData.measurableSet_valid line 157
  19. abbrev OAI.TriangularBilliards.CodedChain line 195

    Source documentation

    Standard-Borel coding of the exact complete trajectories.

    abbrev CodedChain (Q : Triangle) := {a : Phase × ChainData // a.2.Valid Q a.1}
…

    Mentions: OAI.TriangularBilliards.Triangle, OAI.TriangularBilliards.Phase, OAI.TriangularBilliards.ChainData

  20. instance OAI.TriangularBilliards.CodedChain.standardBorel line 199
  21. def OAI.TriangularBilliards.CodedChain.initial line 202
  22. def OAI.TriangularBilliards.CodedChain.chain line 204
  23. instance OAI.TriangularBilliards.CodedChain.nonempty line 206
  24. lemma OAI.TriangularBilliards.CodedChain.initial_injective line 210
  25. lemma OAI.TriangularBilliards.CodedChain.initial_embedding line 219
  26. lemma OAI.TriangularBilliards.CodedChain.range_initial line 222
  27. lemma OAI.TriangularBilliards.CodedChain.measurableSet_regular line 231
  28. def OAI.TriangularBilliards.CodedChain.fromPhase line 237

    Source documentation

    The inverse is Borel by Lusin--Souslin, not by choice of arbitrary unmeasurable representatives. It agrees with every exact chain at its initial state.

    def fromPhase (Q : Triangle) : Phase → CodedChain Q := (initial_embedding Q).invFun

    Mentions: OAI.TriangularBilliards.Triangle, OAI.TriangularBilliards.Phase, OAI.TriangularBilliards.CodedChain, OAI.TriangularBilliards.CodedChain.initial_embedding

  29. lemma OAI.TriangularBilliards.CodedChain.measurable_fromPhase line 239
  30. lemma OAI.TriangularBilliards.CodedChain.fromPhase_initial line 242
  31. def OAI.TriangularBilliards.CodedChain.index line 245
  32. lemma OAI.TriangularBilliards.CodedChain.index_spec line 248
  33. lemma OAI.TriangularBilliards.CodedChain.index_eq_iff line 252
  34. lemma OAI.TriangularBilliards.CodedChain.measurable_time line 260
  35. lemma OAI.TriangularBilliards.CodedChain.measurable_point line 264
  36. lemma OAI.TriangularBilliards.CodedChain.measurable_direction line 268
  37. lemma OAI.TriangularBilliards.CodedChain.measurable_index line 272
  38. lemma OAI.TriangularBilliards.CodedChain.measurable_at line 284
  39. lemma OAI.TriangularBilliards.CodedChain.fromPhase_at line 303
  40. lemma OAI.TriangularBilliards.measurable_billiardFlow line 315

    Source documentation

    Joint Borel measurability of the actual chosen billiard flow, obtained from the unique exact chain, including the singular-set identity convention.

    lemma measurable_billiardFlow (Q : Triangle) :
    Measurable (fun a : ℝ × Phase => billiardFlow Q a.1 a.2) := by
…

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

  41. lemma OAI.TriangularBilliards.measurable_billiardFlow_time line 337