LocalApproximation.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.RuledApproximation.c1_local_remainder line 14

Source documentation

A quantitative derivative remainder in convex local coordinates.

theorem c1_local_remainder {E F : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    [NormedAddCommGroup F] [NormedSpace ℝ F]
    {v : E → F} {U : Set E} (hU : IsOpen U) (hv : ContDiffOn ℝ 1 v U)
    {p : E} (hp : p ∈ U) {delta : ℝ} (hd : 0 < delta) :
    ∃ r : ℝ, 0 < r ∧ ball p r ⊆ U ∧ ∀ x ∈ ball p r, ∀ y ∈ ball p r,
      ‖v x - v y - fderiv ℝ v p (x - y)‖ ≤ delta * ‖x - y‖ := by
…

theorem OAI.RuledApproximation.continuous_nonneg_extension line 34

Source documentation

Extending a nonnegative continuous weight from a compact patch does not alter it there.

theorem continuous_nonneg_extension {E : Type*} [TopologicalSpace E] [NormalSpace E]
    {K : Set E} (hK : IsClosed K) {f : E → ℝ} (hf : ContinuousOn f K)
    (hn : ∀ x ∈ K, 0 ≤ f x) :
    ∃ F : E → ℝ, Continuous F ∧ (∀ x, 0 ≤ F x) ∧ Set.EqOn F f K := by
…

abbrev OAI.RuledApproximation.Parameter line 47
def OAI.RuledApproximation.LatticeModel line 50
Source documentation
Exact affine lattice template. The uniform bound retains finitely many centers.
```
def LatticeModel (A : Parameter →L[ℝ] Parameter) (L R : ℝ) : Prop :=
…
```
Mentions: OAI.RuledApproximation.Parameter

theorem OAI.RuledApproximation.local_finite_certificate line 57

Source documentation

The nonlinear local producer. Unlike tilting a continuum of lines, it produces a finite set of intercept centers covering every label and every time simultaneously.

theorem local_finite_certificate {K U : Set Parameter} (hK : IsCompact K)
    (hU : IsOpen U) (hKU : K ⊆ U) (v : Parameter → Parameter)
    (A : Parameter →L[ℝ] Parameter) {L R delta : ℝ}
    (hL : 0 ≤ L) (hdelta : 0 ≤ delta) (hmodel : LatticeModel A L R)
    (hrem : ∀ p ∈ U, ∀ b ∈ U,
      ‖v p - v b - A (p - b)‖ ≤ delta * ‖p - b‖)
    {F : Parameter → ℝ} (hF : Continuous F) (hFpos : ∀ p, 0 ≤ F p)
    {eps : ℝ} (heps : 0 < eps) :
    ∃ n : ℕ, 0 < n ∧ ∃ S : Set Parameter, S.Finite ∧ S ⊆ U ∧
      (∀ p ∈ K, ∀ r : ℝ, |r| ≤ L → ∃ b ∈ S,
        ‖p + r • v p - (b + r • v b)‖ ≤ (1 / 2 + L * delta * R) / n) ∧
      (∑' b : S, F b) / (n : ℝ) ^ 2 < (∫ p in K, F p) + eps := by
…

Mentions: OAI.RuledApproximation.Parameter, OAI.RuledApproximation.LatticeModel