WeightedReciprocal.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Polynomial weighted bounds for the reciprocal operations occurring in metric inversion and normal reconstruction.

lemma OAI.ClosedSurfaceR4.WeightedEstimates.norm_iteratedFDerivWithin_inv line 13

theorem OAI.ClosedSurfaceR4.WeightedEstimates.WeightedBound.inv_real line 29

Source documentation

Both the input size and inverse denominator enter polynomially at each fixed derivative order. There is no compact-range hypothesis.

theorem WeightedBound.inv_real {U : Set E} (hU : UniqueDiffOn ℝ U)
    {s C K : ℝ} {m : ℕ} {f : E → ℝ}
    (hs : 0 < s) (hC : 1 ≤ C) (hK : 1 ≤ K)
    (hf : ContDiffOn ℝ ∞ f U) (hne : ∀ x ∈ U, f x ≠ 0)
    (hInv : ∀ x ∈ U, ‖(f x)⁻¹‖ ≤ K) (hb : WeightedBound U s m C f) :
    WeightedBound U s m ((m.factorial : ℝ)^2*K^(m+1)*C^m) (fun x => (f x)⁻¹) := by
…

Mentions: OAI.ClosedSurfaceR4.WeightedEstimates.WeightedBound