PolynomialFreeNormal.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Apply the rational and square-root estimates to the actual free normal of an immersed surface, with explicit inverse geometric margins.

def OAI.ClosedSurfaceR4.RealModes.freeNormalInputBudget line 13
def OAI.ClosedSurfaceR4.RealModes.freeNormalBudget line 15
lemma OAI.ClosedSurfaceR4.RealModes.normalBudget_nonneg line 19

theorem OAI.ClosedSurfaceR4.RealModes.polynomial_freeNormal_bound line 27

Source documentation

The coefficient depends polynomially on the two-jet bound and the inverse Gram and normal-length bounds.

theorem polynomial_freeNormal_bound (m : ℕ) :
    ∃ D : ℝ, 1 ≤ D ∧ ∀ {U : Set Base} {F : RField 4}, ContDiff ℝ ∞ F →
      RealModeDomain F U → ∀ {s C K : ℝ}, 0 < s → 1 ≤ C → 1 ≤ K →
      WeightedBound U s m C (realTwoJet F) →
      (∀ x ∈ U, ‖(NormalFrame.gramDet (coordDeriv dx F x) (coordDeriv dy F x))⁻¹‖ ≤ K) →
      (∀ x ∈ U, (realSecond F x ⬝ᵥ realSecond F x)⁻¹ ≤ K) →
      WeightedBound U s m (freeNormalBudget m D C K) (freeNormal F) := by
…

Mentions: OAI.ClosedSurfaceR4.RealModes.RField, OAI.ClosedSurfaceR4.RealModes.RealModeDomain, OAI.ClosedSurfaceR4.RealModes.realTwoJet, OAI.ClosedSurfaceR4.NormalFrame.gramDet, OAI.ClosedSurfaceR4.RealModes.realSecond, OAI.ClosedSurfaceR4.RealModes.freeNormalBudget, OAI.ClosedSurfaceR4.RealModes.freeNormal