OAI/Geometry/SurfaceImmersion/Atlas/TangentMetricBounds.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Apply the finite-tail estimate to the actual two tangent expansions.

  1. def OAI.ClosedSurfaceR4.JetPolynomial.MetricPolynomial.tangentExpression line 12
  2. def OAI.ClosedSurfaceR4.JetPolynomial.MetricPolynomial.tangentFamily line 16
  3. lemma OAI.ClosedSurfaceR4.JetPolynomial.MetricPolynomial.smooth_tangentExpression line 21
  4. lemma OAI.ClosedSurfaceR4.JetPolynomial.MetricPolynomial.order_tangentExpression line 30
  5. lemma OAI.ClosedSurfaceR4.JetPolynomial.MetricPolynomial.represents_tangentExpression line 39
  6. theorem OAI.ClosedSurfaceR4.JetPolynomial.MetricPolynomial.compact_tangent_metric_tail line 56

    Source documentation

    The two choices of tangent yield the xx, xy, and yy metric tails. The exponent is fixed by the finite expression, independently of m.

    theorem compact_tangent_metric_tail {S : TopologicalSpace.Opens Base} {O K : Set LowJet}
    (hO : IsOpen O) (hK : IsCompact K) (hKO : K ⊆ O)
    (X Y : VectorExpression) (R : ℕ → VectorExpression)
    (hXs : X.SmoothCoeffs O) (hYs : Y.SmoothCoeffs O) (hRs : ∀ i, (R i).SmoothCoeffs O)
    (L : ℕ) (hL : 1 ≤ L) (hX : ∀ a, (X a).order ≤ 2) (hY : ∀ a, (Y a).order ≤ 2)
    (hR : ∀ j < L, ∀ a, (R j a).order ≤ 2 * j + 2)
    (dx dy : Fin 2) (b c : Bool) (ℓ : Base →L[ℝ] ℝ) :
    ∃ d : ℕ, ∀ (m : ℕ) (B : ℝ), 1 ≤ B → ∃ D : ℝ, 0 ≤ D ∧
      ∀ (G : Base → Space) (s z : ℝ), 0 < z → z ≤ s → s ≤ 1 →
      ContDiff ℝ ∞ G → Set.MapsTo (lowJet G) S K →
      WeightedBound S s (m + (2 * L + 1)) B (lowJet G) →
      ∀ (g : Geometry (E := R4) S (coordinateVector dy)) (U : ℕ → Family S R4),
…

    Mentions: OAI.ClosedSurfaceR4.JetPolynomial.Base, OAI.ClosedSurfaceR4.JetPolynomial.LowJet, OAI.ClosedSurfaceR4.JetPolynomial.VectorExpression, OAI.ClosedSurfaceR4.JetPolynomial.Space, OAI.ClosedSurfaceR4.JetPolynomial.lowJet, OAI.ClosedSurfaceR4.JetPolynomial.R4, OAI.ClosedSurfaceR4.JetPolynomial.coordinateVector