← Mathematical handbook

Integrable square-root derivatives, including the singular endpoint

noncomputable def Verification.sqrtSlope (b t : ℝ) : ℝ

Equations

• Verification.sqrtSlope b t = b / √(2 * b * t)

theorem Verification.sqrtSlope_nonneg {b : ℝ} (hb : 0 ≤ b) (t : ℝ) : 0 ≤ sqrtSlope b t

theorem Verification.sqrtSlope_intervalIntegrable {b : ℝ} (hb : 0 < b) {v : ℝ} (hv : 0 ≤ v) : IntervalIntegrable (sqrtSlope b) MeasureTheory.volume 0 v

theorem Verification.integral_sqrtSlope {b : ℝ} (hb : 0 < b) {v : ℝ} (hv : 0 ≤ v) : ∫ (t : ℝ) in 0..v, sqrtSlope b t = √(2 * b * v)

theorem Verification.sqrtSlope_integrable {b : ℝ} (hb : 0 < b) : MeasureTheory.Integrable (fun (v : ↑unitInterval) => sqrtSlope b ↑v) MeasureTheory.volume

theorem Verification.integral_sqrtSlope_Iic {b : ℝ} (hb : 0 < b) (v : ↑unitInterval) : ∫ (t : ↑unitInterval) in Set.Iic v, sqrtSlope b ↑t = √(2 * b * ↑v)

theorem Verification.sqrtSlope_reflection_integrable {b : ℝ} (hb : 0 < b) : MeasureTheory.Integrable (fun (v : ↑unitInterval) => sqrtSlope b (1 - ↑v)) MeasureTheory.volume

theorem Verification.integral_sqrtSlope_reflection_Ioc {b : ℝ} (hb : 0 < b) (c v : ↑unitInterval) (hcv : c ≤ v) : ∫ (t : ↑unitInterval) in Set.Ioc c v, sqrtSlope b (1 - ↑t) = √(2 * b * (1 - ↑c)) - √(2 * b * (1 - ↑v))