OAI/Geometry/SurfaceImmersion/Correction/PolynomialRealReconstruction.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A common polynomial bound for every real reconstruction coefficient.

  1. def OAI.ClosedSurfaceR4.RealModes.normalRatioBudget line 13
  2. def OAI.ClosedSurfaceR4.RealModes.reconstructionBudget line 16
  3. lemma OAI.ClosedSurfaceR4.RealModes.reconstructionBudget_bounds line 20
  4. theorem OAI.ClosedSurfaceR4.RealModes.weighted_realJet_coefficients line 49

    Source documentation

    The two inverse bounds concern the Gram determinant and the squared length of the transverse second fundamental form. All derivatives are estimated by explicit polynomials in these bounds and the two-jet bound.

    theorem weighted_realJet_coefficients {U : Set E} (hU : UniqueDiffOn ℝ U)
    {J : E → RealTwoJet} (hJ : ContDiff ℝ ∞ J) {s C K : ℝ} {m : ℕ}
    (hs : 0 < s) (hC : 1 ≤ C) (hK : 1 ≤ K) (bJ : WeightedBound U s m C J)
    (hD : ∀ x ∈ U, NormalFrame.gramDet (J x 0) (J x 1) ≠ 0)
    (hN : ∀ x ∈ U, realJetNormal (J x) 4 ≠ 0)
    (hGD : ∀ x ∈ U, ‖(NormalFrame.gramDet (J x 0) (J x 1))⁻¹‖ ≤ K)
    (hGN : ∀ x ∈ U, ‖(realJetNormal (J x) 4 ⬝ᵥ realJetNormal (J x) 4)⁻¹‖ ≤ K) :
    (∀ i, WeightedBound U s m (reconstructionBudget m C K) (fun x => realScalarCoefficients (J x) i)) ∧
    (∀ i, WeightedBound U s m (reconstructionBudget m C K) (fun x => realVectorCoefficients (J x) i)) := by
…

    Mentions: OAI.ClosedSurfaceR4.RealModes.RealTwoJet, OAI.ClosedSurfaceR4.NormalFrame.gramDet, OAI.ClosedSurfaceR4.RealModes.realJetNormal, OAI.ClosedSurfaceR4.RealModes.reconstructionBudget, OAI.ClosedSurfaceR4.RealModes.realScalarCoefficients, OAI.ClosedSurfaceR4.RealModes.realVectorCoefficients