OAI/Geometry/SurfaceImmersion/Correction/PolynomialNormalBounds.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Explicit polynomial bounds for the Gram determinant, tangential coefficients and normal projection.

  1. def OAI.ClosedSurfaceR4.RealModes.dotBudget line 15
  2. def OAI.ClosedSurfaceR4.RealModes.quadraticBudget line 16
  3. def OAI.ClosedSurfaceR4.RealModes.inverseGramBudget line 17
  4. def OAI.ClosedSurfaceR4.RealModes.liftBudget line 19
  5. def OAI.ClosedSurfaceR4.RealModes.normalBudget line 20
  6. lemma OAI.ClosedSurfaceR4.RealModes.dotBudget_nonneg line 22
  7. lemma OAI.ClosedSurfaceR4.RealModes.quadraticBudget_ge_one line 25
  8. lemma OAI.ClosedSurfaceR4.RealModes.inverseGramBudget_nonneg line 30
  9. lemma OAI.ClosedSurfaceR4.RealModes.liftBudget_nonneg line 35
  10. lemma OAI.ClosedSurfaceR4.RealModes.weighted_quadratic_pair line 42
  11. theorem OAI.ClosedSurfaceR4.RealModes.weighted_realNormalPart line 68

    Source documentation

    Rational normal projection with an explicit polynomial dependence on the inverse Gram bound.

    theorem weighted_realNormalPart {U : Set E} (hU : UniqueDiffOn ℝ U)
    {s C K : ℝ} {m : ℕ} (hs : 0 < s) (hC : 1 ≤ C) (hK : 1 ≤ K)
    {X Y W : E → RVec 4}
    (hX : ContDiffOn ℝ ∞ X U) (hY : ContDiffOn ℝ ∞ Y U) (hW : ContDiffOn ℝ ∞ W U)
    (bX : WeightedBound U s m C X) (bY : WeightedBound U s m C Y)
    (bW : WeightedBound U s m C W)
    (hne : ∀ x ∈ U, NormalFrame.gramDet (X x) (Y x) ≠ 0)
    (hInv : ∀ x ∈ U, ‖(NormalFrame.gramDet (X x) (Y x))⁻¹‖ ≤ K) :
    WeightedBound U s m (normalBudget m C K) (fun x => realNormalPart (X x) (Y x) (W x)) := by
…

    Mentions: OAI.ClosedSurfaceR4.RealModes.RVec, OAI.ClosedSurfaceR4.NormalFrame.gramDet, OAI.ClosedSurfaceR4.RealModes.normalBudget, OAI.ClosedSurfaceR4.RealModes.realNormalPart