OAI/Geometry/RCD/Sobolev/SqrtDerivativeBound.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.abs_sub_le_of_sqrt_derivative_bound_add line 12

   Source documentation

   Integrating a heat-smoothing singularity together with a bounded error.

   theorem abs_sub_le_of_sqrt_derivative_bound_add {F D : ℝ → ℝ} {A B T : ℝ}
       (hT : 0 < T) (hc : ContinuousOn F (Icc 0 T))
       (hd : ∀ t ∈ Ioo 0 T, HasDerivAt F (D t) t)
       (hb : ∀ t ∈ Ioo 0 T, |D t| ≤ A / Real.sqrt t+B) :
       |F T - F 0| ≤ 2*A*Real.sqrt T+B*T := by
   …

2. theorem OAI.RegularPointCoordinates.abs_sub_le_of_sqrt_derivative_bound line 47

   Source documentation

   The integrable singularity of heat smoothing costs exactly a square root of elapsed time. Only continuity is needed at the initial time.

   theorem abs_sub_le_of_sqrt_derivative_bound {F D : ℝ → ℝ} {A T : ℝ}
       (hT : 0 < T) (hc : ContinuousOn F (Icc 0 T))
       (hd : ∀ t ∈ Ioo 0 T, HasDerivAt F (D t) t)
       (hb : ∀ t ∈ Ioo 0 T, |D t| ≤ A / Real.sqrt t) :
       |F T - F 0| ≤ 2*A*Real.sqrt T := by
   …