CycleCorrectedGeometry.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Reference charts give the generic finite geometry for any number of cycles without shrinking the admissible chart radii after that number is chosen. The actual corrected families are then attached to those circles.

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.ReferenceCircularAtlas.finite_copy_geometry line 32

Source documentation

Use the already selected full-disk reference charts, for arbitrarily many copies, rather than choosing a new admissible radius after the copy count.

theorem finite_copy_geometry {ι : Type*} [Fintype ι] [DecidableEq ι]
    (index : ι → d.B.centers) (component : ι → Fin 3)
    (lo hi : ι → ℝ) (hlo : ∀ a, 0 < lo a) (hlohi : ∀ a, lo a < hi a)
    (hhi : ∀ a, hi a < d.radius (index a))
    {eta : ℝ} (heta : 0 < eta) :
    ∃ q : CircularFamilyGeometry d.B ι,
      (∀ a, lo a < q.radius a ∧ q.radius a < hi a) ∧
      (∀ a, (q.curves a).index = index a) ∧
      (∀ a, q.outerRadius a = d.radius (index a)) ∧
      (∀ a, q.chartRadius a = d.radius (index a)) ∧
      (∀ a, q.convexPart a = d.L (index a)) ∧
      (∀ a, ‖q.linearPart a-(d.P (index a)).ξ (component a)‖ < eta) ∧
…

Mentions: OAI.ClosedSurfaceR4.FiniteOrderSmoothing.CircularFamilyGeometry

def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothPrimitiveFamily.reindex line 107
Source documentation
Reindex only the genuine finite family, preserving its exact sum.
```
def reindex (f : SmoothPrimitiveFamily ι u) (e : κ ≃ ι) : SmoothPrimitiveFamily κ u where
…
```
Mentions: OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothPrimitiveFamily
def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.CircularFamilyGeometry.copiedPhases line 123
Source documentation
The actual restored phase, allowing repeated copies of a chart.
```
def copiedPhases (q : CircularFamilyGeometry B ι) (a : ι) : M → ℝ :=
…
```
Mentions: OAI.ClosedSurfaceR4.FiniteOrderSmoothing.CircularFamilyGeometry
lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.CircularFamilyGeometry.copiedPhases_germ line 127

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.CircularFamilyGeometry.with_cycle_families line 153

Source documentation

Attach cycle amplitudes without changing any selected generic geometry.

theorem with_cycle_families {N m : ℕ} (q : CircularFamilyGeometry B (Fin (N*m)))
    {u : ∀ p : M, CovariantTwoTensor p}
    (f : Fin N → SmoothPrimitiveFamily (Fin m) u) (hN : 0 < N)
    (hamp : ∀ k a p, 0 ≤ (f k).amplitude a p)
    (hpos : ∀ a p, 0 < (f a.divNat).amplitude a.modNat p ↔
      p ∈ circularCoordinateDisk ((q.curves a).index : M) (q.radius a))
    (hphase : ∀ a, (f a.divNat).phase a.modNat = q.copiedPhases a)
    (houter : ∀ i p, p ∈ tsupport (B.weight i) → B.outer i =ᶠ[𝓝 p] (fun _ => 1)) :
    ∃ D : CircularPrimitiveFamily B (Fin (N*m)),
      D.curves = q.curves ∧ D.radius = q.radius ∧ D.outerRadius = q.outerRadius ∧
      D.chartRadius = q.chartRadius ∧ D.linearPart = q.linearPart ∧ D.convexPart = q.convexPart ∧
      (∀ a p, D.amplitude a p = (f a.divNat).cycleAmplitude N a.modNat p) ∧
…

Mentions: OAI.ClosedSurfaceR4.FiniteOrderSmoothing.CircularFamilyGeometry, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.CovariantTwoTensor, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothPrimitiveFamily, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.circularCoordinateDisk, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.CircularPrimitiveFamily

def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.ReferenceCircularAtlas.cycleLinearParts line 194
def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.ReferenceCircularAtlas.cycleWeights line 198

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.ReferenceCircularAtlas.corrected_cycles line 206

Source documentation

One radius box and map neighborhood precede every cycle count. The output retains the actual amplitude formula and fixed cutoff bounds, so the uniform C1 estimate can be applied without choosing further constants.

theorem corrected_cycles {F : M → Space}
    (hF : ContMDiff planeModel spaceModel ∞ F) (r : ℝ)
    (href : gref.inner = g.inner-inducedTensor (r • F))
    {phaseBound weightBound mapBound : ℝ}
    (hphaseBound : 0 < phaseBound) (hweightBound : 0 < weightBound)
    (hmapBound : 0 < mapBound)
    {m : ℕ} (e : Fin m ≃ (d.B.centers × Fin 3)) :
    ∃ (mapTol delta : ℝ) (W : ℕ → ℝ),
      0 < mapTol ∧ mapTol ≤ mapBound ∧ 0 < delta ∧
      (∀ i, delta ≤ d.radius i/2) ∧ (∀ j, 0 ≤ W j) ∧
      ∀ N : ℕ, 0 < N →
      ∃ q : CircularFamilyGeometry d.B (Fin (N*m)),
…

Mentions: OAI.ClosedSurfaceR4.Space, OAI.ClosedSurfaceR4.planeModel, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.inducedTensor, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.CircularFamilyGeometry