Differentiate Integral Mul Test Function #
Supporting results for the Constantin–Ignatova–Vicol axisymmetric regularity theorem.
theorem
CIV.hasDerivAt_integral_mul_testfunction_of_dominated
{Θ D : ℝ × ℝ → ℝ → ℝ}
{ψ bound : ℝ × ℝ → ℝ}
{s : Set ℝ}
{τ₀ : ℝ}
(hs : s ∈ nhds τ₀)
(hF_meas :
∀ᶠ (τ : ℝ) in nhds τ₀, MeasureTheory.AEStronglyMeasurable (fun (y : ℝ × ℝ) => Θ y τ * ψ y) MeasureTheory.volume)
(hF_int : MeasureTheory.Integrable (fun (y : ℝ × ℝ) => Θ y τ₀ * ψ y) MeasureTheory.volume)
(hF'_meas : MeasureTheory.AEStronglyMeasurable (fun (y : ℝ × ℝ) => D y τ₀ * ψ y) MeasureTheory.volume)
(h_bound : ∀ᵐ (y : ℝ × ℝ), ∀ τ ∈ s, |D y τ * ψ y| ≤ bound y)
(h_bound_int : MeasureTheory.Integrable bound MeasureTheory.volume)
(h_diff : ∀ᵐ (y : ℝ × ℝ), ∀ τ ∈ s, HasDerivAt (fun (τ' : ℝ) => Θ y τ' * ψ y) (D y τ * ψ y) τ)
:
Differentiation under the integral sign for a τ-parametrised field paired against a fixed
function ψ (a smooth compactly-supported test function in the intended use, though nothing here
needs that) — the step that turns a pointwise-in-τ derivative bound coming from the zoom PDE
into an actual derivative of the paired integral ∫ y, Θ (y, τ) ψ y, which the two-point Lipschitz
bound of CIV.abs_sub_le_of_hasDerivWithinAt_le_abs then turns into the shape "the time-pairing
estimate hpair" needs.
theorem
CIV.hasDerivAt_integral_mul_testfunction_of_dominated_univ
{Θ D : ℝ × ℝ → ℝ → ℝ}
{ψ bound : ℝ × ℝ → ℝ}
{τ₀ : ℝ}
(hF_meas :
∀ᶠ (τ : ℝ) in nhds τ₀, MeasureTheory.AEStronglyMeasurable (fun (y : ℝ × ℝ) => Θ y τ * ψ y) MeasureTheory.volume)
(hF_int : MeasureTheory.Integrable (fun (y : ℝ × ℝ) => Θ y τ₀ * ψ y) MeasureTheory.volume)
(hF'_meas : MeasureTheory.AEStronglyMeasurable (fun (y : ℝ × ℝ) => D y τ₀ * ψ y) MeasureTheory.volume)
(h_bound : ∀ᵐ (y : ℝ × ℝ), ∀ (τ : ℝ), |D y τ * ψ y| ≤ bound y)
(h_bound_int : MeasureTheory.Integrable bound MeasureTheory.volume)
(h_diff : ∀ᵐ (y : ℝ × ℝ), ∀ (τ : ℝ), HasDerivAt (fun (τ' : ℝ) => Θ y τ' * ψ y) (D y τ * ψ y) τ)
:
Specialisation of hasDerivAt_integral_mul_testfunction_of_dominated to the case where the
neighbourhood s is all of ℝ.