Geometry.lean`

39 declarations, 0 contain sorry, 0 declared as axioms

Torus coordinate equivalence, smooth passage geometry, and all-jet passage convergence.

def OAI.ThreeTorus.torusTriple line 25
lemma OAI.ThreeTorus.torusTriple_apply line 30
lemma OAI.ThreeTorus.torusTriple_symm_apply line 32
lemma OAI.ThreeTorus.measurePreserving_torusTriple line 36
def OAI.ThreeTorus.torusPassage line 41
lemma OAI.ThreeTorus.torusPassage_apply line 44
lemma OAI.ThreeTorus.torusPassage_symm_apply line 50
lemma OAI.ThreeTorus.measurePreserving_torusPassage line 56
def OAI.ThreeTorus.passageLift line 61
def OAI.ThreeTorus.passageInverseLift line 64
lemma OAI.ThreeTorus.contDiff_passageLift line 67
lemma OAI.ThreeTorus.contDiff_passageInverseLift line 79
lemma OAI.ThreeTorus.smooth_torusPassage line 91
lemma OAI.ThreeTorus.smooth_torusPassage_symm line 105
lemma OAI.ThreeTorus.contDiff_real_primitive line 126
lemma OAI.ThreeTorus.primitive_translate_one line 138
lemma OAI.ThreeTorus.periodic_primitive_mod line 143
lemma OAI.ThreeTorus.continuous_periodic_lift line 153

def OAI.ThreeTorus.circlePrimitive line 158

Source documentation

The precise globally defined circle-valued primitive used by a passage.

def circlePrimitive {v : ℝ → ℝ} (hv : Function.Periodic v 1)
    (hc : Continuous v) {k : ℤ} (hk : (∫ t in 0..1, v t) = k) : UnitAddCircle → UnitAddCircle :=
…

lemma OAI.ThreeTorus.circlePrimitive_coe line 162
lemma OAI.ThreeTorus.continuous_circlePrimitive line 166
def OAI.ThreeTorus.circleSpeed line 172
lemma OAI.ThreeTorus.circleSpeed_coe line 175
lemma OAI.ThreeTorus.continuous_circleSpeed line 178

lemma OAI.ThreeTorus.primitive_passage_properties line 184

Source documentation

Global C-infinity, inverse C-infinity, and exact Haar preservation for the manuscript passage, without assuming any geometric conclusion.

lemma primitive_passage_properties {v s : ℝ → ℝ}
    (hv : Function.Periodic v 1) (hs : Function.Periodic s 1)
    (hvc : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) v)
    (hsc : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) s)
    {k : ℤ} (hk : (∫ t in 0..1, v t) = k) :
    let T := torusPassage (circlePrimitive hv hvc.continuous hk) (circleSpeed hs)
…

Mentions: OAI.ThreeTorus.torusPassage, OAI.ThreeTorus.circlePrimitive, OAI.ThreeTorus.circleSpeed

lemma OAI.ThreeTorus.passage_rounding line 206
Source documentation
The bounded winding correction; no subsequence of passage integers is needed.
```
lemma passage_rounding (A : ℝ) {N : ℕ} (hN : 0 < N) :
    ∃ d : ℝ, ∃ k : ℤ, |d| ≤ (N:ℝ)⁻¹ ∧ (N:ℝ)*(A+d) = k := by
…
```
lemma OAI.ThreeTorus.passage_rounded_slope line 221
lemma OAI.ThreeTorus.passage_speed_smooth line 234

lemma OAI.ThreeTorus.exists_rounded_passage line 242

Source documentation

Existence of the exact smooth Haar-preserving passage for each integer N>0. The map is the manuscript formula with H_N'=N(V+Delta_N) and sigma_N=1/N+J/N^2.

lemma exists_rounded_passage {v J : ℝ → ℝ}
    (hv : Function.Periodic v 1) (hJ : Function.Periodic J 1)
    (hvc : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) v)
    (hJc : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) J)
    {N : ℕ} (hN : 0 < N) :
    ∃ d : ℝ, ∃ T : Equiv.Perm Torus,
      |d| ≤ (N:ℝ)⁻¹ ∧ Smooth T ∧ Smooth T.symm ∧ MeasurePreserving T μ μ ∧
      ∀ x : Cover, T (project x) = project (passageLift
        (fun u => ∫ t in 0..u, (N:ℝ)*(v t+d))
        (fun a => (N:ℝ)⁻¹+(N:ℝ)⁻¹^2*J a) x) := by
…

Mentions: OAI.ThreeTorus.Torus, OAI.ThreeTorus.Smooth, OAI.ThreeTorus.μ, OAI.ThreeTorus.Cover, OAI.ThreeTorus.project, OAI.ThreeTorus.passageLift

lemma OAI.ThreeTorus.iteratedFDeriv_slice line 278
lemma OAI.ThreeTorus.continuous_iteratedFDeriv_slice line 292

lemma OAI.ThreeTorus.smooth_parameter_jets_tendsto line 304

Source documentation

Joint smoothness gives convergence in every C^k seminorm on compact sets.

lemma smooth_parameter_jets_tendsto
    {P E G : Type*} [NormedAddCommGroup P] [NormedSpace ℝ P] [ProperSpace P]
    [NormedAddCommGroup E] [NormedSpace ℝ E]
    [NormedAddCommGroup G] [NormedSpace ℝ G]
    {F : P × E → G} (hF : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) F)
    (p : P) {K : Set E} (hK : IsCompact K) (n : ℕ) :
    TendstoUniformlyOn (fun a x => iteratedFDeriv ℝ n (fun y => F (a,y)) x)
      (fun x => iteratedFDeriv ℝ n (fun y => F (p,y)) x) (𝓝 p) K := by
…

def OAI.ThreeTorus.passageFamily line 328
Source documentation
A nonsingular two-parameter form of the exact passage lift (both signs).
```
def passageFamily (v J : ℝ → ℝ) (r : ℝ) (p : ℝ × ℝ) (x : Cover) : Cover :=
…
```
Mentions: OAI.ThreeTorus.Cover
lemma OAI.ThreeTorus.smooth_passageFamily line 333
lemma OAI.ThreeTorus.passageFamily_zero line 357
lemma OAI.ThreeTorus.passageFamily_increment line 362

lemma OAI.ThreeTorus.passageLift_eq_family line 387

Source documentation

The passage and inverse are specializations of the same smooth family.

lemma passageLift_eq_family {v J : ℝ → ℝ} (hv : Continuous v)
    {N : ℕ} (hN : 0 < N) (d : ℝ) :
    passageLift (fun u => ∫ t in 0..u, (N:ℝ)*(v t+d))
      (fun a => (N:ℝ)⁻¹+(N:ℝ)⁻¹^2*J a) = passageFamily v J 1 ((N:ℝ)⁻¹,d) ∧
    passageInverseLift (fun u => ∫ t in 0..u, (N:ℝ)*(v t+d))
      (fun a => (N:ℝ)⁻¹+(N:ℝ)⁻¹^2*J a) = passageFamily v J (-1) ((N:ℝ)⁻¹,d) := by
…

Mentions: OAI.ThreeTorus.passageLift, OAI.ThreeTorus.passageFamily, OAI.ThreeTorus.passageInverseLift

lemma OAI.ThreeTorus.passage_parameters_tendsto line 413

lemma OAI.ThreeTorus.passage_Cinfty_limit line 425

Source documentation

All spatial derivatives of each sign of the passage converge uniformly on any fixed compact set. This is genuine C-infinity convergence, not C-zero.

lemma passage_Cinfty_limit {v J : ℝ → ℝ}
    (hv : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) v)
    (hJ : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) J)
    {d : ℕ → ℝ} (hd : ∀ N : ℕ, 0 < N → |d N| ≤ (N:ℝ)⁻¹)
    (r : ℝ) {K : Set Cover} (hK : IsCompact K) (n : ℕ) :
    TendstoUniformlyOn
      (fun (N : ℕ) x => iteratedFDeriv ℝ n (passageFamily v J r ((N:ℝ)⁻¹,d N)) x)
      (fun x => iteratedFDeriv ℝ n (fun y : Cover => ![y 0+r*v (y 1),y 1,y 2]) x)
      atTop K := by
…

Mentions: OAI.ThreeTorus.Cover, OAI.ThreeTorus.passageFamily