PointedDualLimit.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Local dual feasibility in the Euclidean limit

theorem OAI.RegularPointCoordinates.pointed_lift_dist_tendsto line 13

theorem OAI.RegularPointCoordinates.pointed_dual_limit line 33

Source documentation

Dual inequalities are preserved on the whole open working ball. The assumptions here are the actual uniform values of the two source potentials.

theorem pointed_dual_limit {n : ℕ} {S : ℝ}
    (p : ℕ → X) (r ε : ℕ → ℝ) (v : ℕ → X → Euclidean n)
    (hεlim : Tendsto ε atTop (𝓝 0))
    (hv : ∀ k, IsPointedApproximation (p k) 0 (r k) S (ε k) (v k))
    (φ ψ : ℕ → X → ℝ) {f g : Euclidean n → ℝ}
    (hf : Continuous f) (hg : Continuous g)
    (hφ : ∀ δ : ℝ, 0<δ → ∀ᶠ k in atTop, ∀ x,
      dist x (p k)≤S*r k → |φ k x-f (v k x)|<δ)
    (hψ : ∀ δ : ℝ, 0<δ → ∀ᶠ k in atTop, ∀ x,
      dist x (p k)≤S*r k → |ψ k x-g (v k x)|<δ)
    (had : ∀ k x y, φ k x+ψ k y≤(dist x y/r k)^2/2)
    {a b : Euclidean n} (ha : ‖a‖<S) (hb : ‖b‖<S) :
…

Mentions: OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.IsPointedApproximation