Time weights

Derivatives and integrals of functions of -s for s < 0. These appear in the proof of the time-weighted energy inequality (lem:aniso:closure in the paper).

theorem CIV.hasDerivAt_neg_rpow {η t : ℝ} (ht : t < 0) : HasDerivAt (fun (s : ℝ) => (-s) ^ η) (-(η * (-t) ^ (η - 1))) t

The derivative of s ↦ (-s)^η at a negative point t.

theorem CIV.integral_inv_neg {a b : ℝ} (ha : a < b) (hb : b < 0) : ∫ (s : ℝ) in a..b, (-s)⁻¹ = Real.log (-a) - Real.log (-b)

Integral of (-s)⁻¹ over [a, b] for a < b < 0.

theorem CIV.integral_neg_rpow {a b β : ℝ} (ha : a < b) (hb : b ≤ 0) (hβ : β < 1) : ∫ (s : ℝ) in a..b, (-s) ^ (-β) = ((-a) ^ (1 - β) - (-b) ^ (1 - β)) / (1 - β)

Integral of (-s)^(-β) over [a, b] for a < b ≤ 0 and β < 1.

theorem CIV.exp_integral_inv_neg {a b c : ℝ} (ha : a < b) (hb : b < 0) (hc : 0 ≤ c) : Real.exp (∫ (s : ℝ) in a..b, c * (-s)⁻¹) = (-a / -b) ^ c

Exponential of the integral of c * (-s)⁻¹ over [a, b] for a < b < 0 and c ≥ 0.