OAI/Analysis/AffineBernstein/SmoothCapTest.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.AffineBernstein.smoothCapTest line 15

   Source documentation

   A smooth convex cap test, quadratic below the fixed transition interval and identically zero above it.

   def smoothCapTest (ε b t : ℝ) : ℝ :=
   …

2. lemma OAI.AffineBernstein.smoothCapTest_hasDeriv line 18
3. lemma OAI.AffineBernstein.smoothCapTest_second line 29
4. lemma OAI.AffineBernstein.smoothCapTest_smooth line 39
5. lemma OAI.AffineBernstein.smoothCapTest_second_nonneg line 46
6. lemma OAI.AffineBernstein.smoothCapTest_second_one line 51
7. lemma OAI.AffineBernstein.smoothCapTest_vanish line 56
8. lemma OAI.AffineBernstein.smoothCapTest_lower_order_bound line 76

   Source documentation

   All lower-order terms of the cap identity are bounded by a single constant fixed by the level interval, center level, dimension and cutoff. Thus the test construction requires no solution-dependent constant.

   lemma smoothCapTest_lower_order_bound (n : ℕ) (ε b a q₀ : ℝ) :
       ∃ C > 0, ∀ t ∈ Set.Icc a (b+ε),
         (n:ℝ)*(t-q₀)*deriv (smoothCapTest ε b) t +
           (n:ℝ)*((n:ℝ)+1)*smoothCapTest ε b t ≤ C := by
   …

   Mentions: OAI.AffineBernstein.smoothCapTest

9. lemma OAI.AffineBernstein.ball_support_lower line 95

   Source documentation

   The quantitative supporting-plane inequality for an actual interior ball, valid in any real normed ambient space.

   lemma ball_support_lower {V : Type*} [NormedAddCommGroup V] [NormedSpace ℝ V]
       (ell : V →L[ℝ] ℝ) (o p : V) {r : ℝ} (hr : 0 < r)
       (hs : ∀ z ∈ Metric.closedBall o r, 0 ≤ ell (z-p)) :
       r*‖ell‖ ≤ ell (o-p) := by
   …