Generators.lean`

21 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.TriangularBilliards.DoubleL2 line 27
def OAI.TriangularBilliards.geodesicHilbertFlow line 30
Source documentation
The actual unitary geodesic dynamics on the oriented double.
```
def geodesicHilbertFlow (Q : Triangle) : HilbertFlow (DoubleL2 Q) where
…
```
Mentions: OAI.TriangularBilliards.Triangle, OAI.TriangularBilliards.DoubleL2
lemma OAI.TriangularBilliards.geodesic_koopman_ae line 52
def OAI.TriangularBilliards.doubleLift line 57
Source documentation
Pullback from the billiard phase space preserves L² exactly.
```
def doubleLift (Q : Triangle) : Lp ℂ 2 (phaseMeasure Q) →ₗᵢ[ℂ] DoubleL2 Q :=
…
```
Mentions: OAI.TriangularBilliards.Triangle, OAI.TriangularBilliards.phaseMeasure, OAI.TriangularBilliards.DoubleL2
lemma OAI.TriangularBilliards.doubleLift_ae line 62
lemma OAI.TriangularBilliards.doubleLift_invariant line 66
lemma OAI.TriangularBilliards.continuous_doubleRotate_angle line 85
lemma OAI.TriangularBilliards.ae_continuousAt_doubleRotate_angle line 93
lemma OAI.TriangularBilliards.continuous_angular_koopman line 97
def OAI.TriangularBilliards.angularHilbertFlow line 106
Source documentation
Rotation of the oriented tangent fiber, not a rotation of the physical velocity with the same sign on both copies.
```
def angularHilbertFlow (Q : Triangle) : HilbertFlow (DoubleL2 Q) where
…
```
Mentions: OAI.TriangularBilliards.Triangle, OAI.TriangularBilliards.DoubleL2
def OAI.TriangularBilliards.transverseHilbertFlow line 130
Source documentation
The transverse geodesic flow is actual geodesic motion after a quarter turn and restoration of the direction, with no global commutation assumed.
```
def transverseHilbertFlow (Q : Triangle) : HilbertFlow (DoubleL2 Q) :=
…
```
Mentions: OAI.TriangularBilliards.Triangle, OAI.TriangularBilliards.DoubleL2
def OAI.TriangularBilliards.SeamCompatible line 142
Source documentation
Seam gluing in the two planar sheets: reflection of base and velocity changes the sheet. This is a local equality, not an assumption of transport invariance or of an analytic estimate.
```
def SeamCompatible (Q : Triangle) (f : DoublePhase → ℂ) : Prop :=
…
```
Mentions: OAI.TriangularBilliards.Triangle, OAI.TriangularBilliards.DoublePhase
def OAI.TriangularBilliards.xDerivative line 147
Source documentation
Horizontal derivative in the actual unit velocity direction.
```
def xDerivative (f : DoublePhase → ℂ) (z : DoublePhase) : ℂ :=
…
```
Mentions: OAI.TriangularBilliards.DoublePhase
lemma OAI.TriangularBilliards.wallReflection_add_smul line 150
lemma OAI.TriangularBilliards.FlightChain.reflected_direction_previous line 156
lemma OAI.TriangularBilliards.FlightChain.reflected_outgoing_line line 163
lemma OAI.TriangularBilliards.seam_orbit_eventually_line line 173
Source documentation
A seam-compatible field has one smooth planar formula through each collision. Thus no trace at a vertex and no angular regularity is needed for the ordinary one-variable calculus along a nonsingular orbit.
```
lemma seam_orbit_eventually_line {Q : Triangle} {z : DoublePhase}
    (c : FlightChain Q z.1) {f : DoublePhase → ℂ} (hf : SeamCompatible Q f)
    (t : ℝ) :
    ∃ n : ℤ, c.time n ≤ t ∧ t < c.time (n + 1) ∧
      (fun s => f (doubleFlow Q s z)) =ᶠ[𝓝 t]
        (fun s => f ((c.point n + (s - c.time n) • (c.direction n : ℂ), c.direction n),
          (n : ZMod 2) + z.2)) := by
…
```
Mentions: OAI.TriangularBilliards.Triangle, OAI.TriangularBilliards.DoublePhase, OAI.TriangularBilliards.FlightChain, OAI.TriangularBilliards.SeamCompatible, OAI.TriangularBilliards.doubleFlow
lemma OAI.TriangularBilliards.seam_orbit_hasDerivAt line 209
lemma OAI.TriangularBilliards.seam_orbit_norm_deriv_le line 227
lemma OAI.TriangularBilliards.seam_orbit_lipschitz line 238

lemma OAI.TriangularBilliards.Analysis.koopman_hasDerivAt_zero line 258

Source documentation

Dominated passage from pointwise orbit derivatives to an actual L² strong derivative. A uniform Lipschitz bound is supplied by the genuine seam-glued spatial calculus; no generator identity is assumed.

lemma koopman_hasDerivAt_zero
    (F : ℝ → A → A) (hm : ∀ t, MeasurePreserving (F t) μ μ)
    (hzero : ∀ x, F 0 x = x)
    {f g : A → ℂ} (hf : MemLp f 2 μ) (hg : MemLp g 2 μ)
    {C : ℝ≥0}
    (hd : ∀ᵐ x ∂μ, HasDerivAt (fun t => f (F t x)) (g x) 0)
    (hbound : ∀ᵐ x ∂μ, LipschitzWith C (fun t => f (F t x)))
    (hgC : ∀ᵐ x ∂μ, ‖g x‖ ≤ C) :
    HasDerivAt (fun t => koopman F hm t (hf.toLp f)) (hg.toLp g) 0 := by
…

Mentions: OAI.TriangularBilliards.Analysis.koopman