← Mathematical handbook

Differentiation of the exact tail corrections, including the joining point

theorem Verification.hasDerivAt_positivePart_sq (x : ℝ) : HasDerivAt (fun (y : ℝ) => max 0 y ^ 2) (2 * max 0 x) x

theorem Verification.hasDerivAt_nuTail (b t : ℝ) : HasDerivAt (fun (a : ℝ) => nuTail a t) (6 * t ^ 2 * max 0 (b * t - 1)) b

theorem Verification.hasDerivAt_xiTail (b t : ℝ) : HasDerivAt (fun (a : ℝ) => xiTail a t) (b * (6 * t ^ 2 * max 0 (b * t - 1))) b

theorem Verification.hasDerivAt_integral_compact {α : Type u_1} [TopologicalSpace α] [CompactSpace α] [MeasurableSpace α] [BorelSpace α] (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] (f g : ℝ → α → ℝ) (hf : Continuous (Function.uncurry f)) (hg : Continuous (Function.uncurry g)) (hd : ∀ (x : ℝ) (a : α), HasDerivAt (fun (y : ℝ) => f y a) (g x a) x) (x : ℝ) : HasDerivAt (fun (y : ℝ) => ∫ (a : α), f y a ∂μ) (∫ (a : α), g x a ∂μ) x

A continuously varying derivative on a compact integration domain can be integrated.

theorem Verification.hasDerivAt_integral_nuTail (b : ℝ) : HasDerivAt (fun (a : ℝ) => ∫ (p : ↑unitInterval × ↑unitInterval), nuTail a |squareDelta p|) (∫ (p : ↑unitInterval × ↑unitInterval), 6 * |squareDelta p| ^ 2 * max 0 (b * |squareDelta p| - 1)) b

theorem Verification.hasDerivAt_integral_xiTail (b : ℝ) : HasDerivAt (fun (a : ℝ) => ∫ (p : ↑unitInterval × ↑unitInterval), xiTail a |squareDelta p|) (b * ∫ (p : ↑unitInterval × ↑unitInterval), 6 * |squareDelta p| ^ 2 * max 0 (b * |squareDelta p| - 1)) b