OAI/Geometry/SurfaceImmersion/Atlas/LocalAnsatzMetricLimit.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Family.compact_value_bound line 21

   Source documentation

   Local smoothness and periodicity suffice for a compact uniform value bound; the local family need not be smooth across the boundary of its domain.

   lemma Family.compact_value_bound (U : Family O E) {Q : Set A}
       (hQ : IsCompact Q) (hQO : Q ⊆ O) :
       ∃ B : ℝ, 0 ≤ B ∧ ∀ p ∈ Q, ∀ t : Period, ‖U.val p t‖ ≤ B := by
   …

   Mentions: OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Family

2. lemma OAI.ClosedSurfaceR4.LocalPeriodicExpansion.inner_error_bound line 38
3. lemma OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Geometry.leading_metric_values line 70

   Source documentation

   The circular velocity law makes the leading metric independent of its fast phase, including the mixed coefficient.

   lemma leading_metric_values {p : A} (hp : p ∈ O) (t : Period) :
       inner ℝ (g.longitudinal.val p t) (g.longitudinal.val p t) =
         inner ℝ (g.X₀ p) (g.X₀ p)+g.q p ∧
       inner ℝ (g.longitudinal.val p t) (g.Y p) = inner ℝ (g.X₀ p) (g.Y p) := by
   …

4. lemma OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Geometry.leading_metric_increment line 89

   Source documentation

   Relative to the old immersion, the leading metric increases precisely the longitudinal coefficient by the velocity variance.

   lemma leading_metric_increment {F : A → E} (dx : A)
       (hX : ∀ p ∈ O, fderiv ℝ F p dx = g.X₀ p+average (g.V.val p))
       (hY : ∀ p ∈ O, fderiv ℝ F p dy = g.Y p)
       {p : A} (hp : p ∈ O) (t : Period) :
       inner ℝ (g.longitudinal.val p t) (g.longitudinal.val p t) =
         inner ℝ (fderiv ℝ F p dx) (fderiv ℝ F p dx)+
           (g.q p-inner ℝ (average (g.V.val p)) (average (g.V.val p))) ∧
       inner ℝ (g.longitudinal.val p t) (g.Y p) =
         inner ℝ (fderiv ℝ F p dx) (fderiv ℝ F p dy) := by
   …

5. theorem OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Geometry.compact_initial_ansatz_metric line 118

   Source documentation

   The three actual metric coefficients approach the old pullback metric plus the variance in the phase direction, uniformly at linear rate in z.

   theorem compact_initial_ansatz_metric {F : A → E} (hF : ContDiff ℝ ∞ F)
       (U : ℕ → Family O E)
       (hU : ∀ i, ContDiff ℝ ∞ (fun y : A × ℝ => (U i).val y.1 (y.2 : Period)))
       (hinit : U 0 = g.initial) {Q : Set A} (hQ : IsCompact Q) (hQO : Q ⊆ O)
       (ℓ : A →L[ℝ] ℝ) (dx : A) (hx : ℓ dx = 1) (hy : ℓ dy = 0)
       (hX : ∀ p ∈ O, fderiv ℝ F p dx = g.X₀ p+average (g.V.val p))
       (hY : ∀ p ∈ O, fderiv ℝ F p dy = g.Y p) (n : ℕ) :
       ∃ C : ℝ, 0 ≤ C ∧ ∀ z : ℝ, 0 < z → z ≤ 1 → ∀ p ∈ Q,
         let f := finiteAnsatz F U ℓ (n+1) z
   …

   Mentions: OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Family, OAI.ClosedSurfaceR4.LocalPeriodicExpansion.finiteAnsatz

6. theorem OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Geometry.compact_initial_ansatz_metric_amplitude line 164

   Source documentation

   The usual amplitude normalization identifies the variance with a², so the limiting metric is the prescribed rank-one metric increment.

   theorem compact_initial_ansatz_metric_amplitude {F : A → E} (hF : ContDiff ℝ ∞ F)
       (U : ℕ → Family O E)
       (hU : ∀ i, ContDiff ℝ ∞ (fun y : A × ℝ => (U i).val y.1 (y.2 : Period)))
       (hinit : U 0 = g.initial) {Q : Set A} (hQ : IsCompact Q) (hQO : Q ⊆ O)
       (ℓ : A →L[ℝ] ℝ) (dx : A) (hx : ℓ dx = 1) (hy : ℓ dy = 0)
       (hX : ∀ p ∈ O, fderiv ℝ F p dx = g.X₀ p+average (g.V.val p))
       (hY : ∀ p ∈ O, fderiv ℝ F p dy = g.Y p) (a : A → ℝ)
       (ha : ∀ p ∈ Q, g.q p-inner ℝ (average (g.V.val p)) (average (g.V.val p)) = a p^2)
       (n : ℕ) :
       ∃ C : ℝ, 0 ≤ C ∧ ∀ z : ℝ, 0 < z → z ≤ 1 → ∀ p ∈ Q,
         let f := finiteAnsatz F U ℓ (n+1) z
   …

   Mentions: OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Family, OAI.ClosedSurfaceR4.LocalPeriodicExpansion.finiteAnsatz