PolynomialUnitPerpBounds.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Quantitative bounds for the actual unit perpendicular vector.

theorem OAI.ClosedSurfaceR4.RealModes.weighted_unitPerp line 15

Source documentation

The only denominator parameter is an upper bound for the reciprocal squared length of the perpendicular product.

theorem weighted_unitPerp (m : ℕ) :
    ∃ D : ℝ, 1 ≤ D ∧ ∀ {U : Set E}, UniqueDiffOn ℝ U →
    ∀ {s C K : ℝ} {X Y B : E → RVec 4}, 0 < s → 0 ≤ C → 1 ≤ K →
      ContDiffOn ℝ ∞ X U → ContDiffOn ℝ ∞ Y U → ContDiffOn ℝ ∞ B U →
      WeightedBound U s m C X → WeightedBound U s m C Y → WeightedBound U s m C B →
      (∀ x ∈ U, 0 < NormalFrame.perpProduct (X x) (Y x) (B x) ⬝ᵥ
        NormalFrame.perpProduct (X x) (Y x) (B x)) →
      (∀ x ∈ U, (NormalFrame.perpProduct (X x) (Y x) (B x) ⬝ᵥ
        NormalFrame.perpProduct (X x) (Y x) (B x))⁻¹ ≤ K) →
      WeightedBound U s m
        (2^m*((m.factorial : ℝ)*D*K^(m+1)*(1+dotBudget m (perpBudget m C))^m)*perpBudget m C)
        (fun x => NormalFrame.unitPerp (X x) (Y x) (B x)) := by
…

Mentions: OAI.ClosedSurfaceR4.RealModes.RVec, OAI.ClosedSurfaceR4.NormalFrame.perpProduct, OAI.ClosedSurfaceR4.RealModes.dotBudget, OAI.ClosedSurfaceR4.RealModes.perpBudget, OAI.ClosedSurfaceR4.NormalFrame.unitPerp