Integrating complementary power bounds

A singular integrand can have two useful estimates: a power integrable at zero, and a power integrable at infinity. Splitting at an arbitrary positive scale gives a bound independent of the upper integration endpoint. This is useful for Hölder estimates of heat potentials, where the scale is the square of the spatial separation.

The endpoint-singular form TauCeti.norm_integral_le_of_ae_norm_le_rpow reverses time and specializes the scale to obtain a bound proportional to the spatial separation to the Hölder exponent.

The one-sided estimates TauCeti.intervalIntegral.intervalIntegrable_of_norm_le_mul_sub_rpow_right and TauCeti.intervalIntegral.norm_integral_le_of_norm_le_mul_sub_rpow_right treat a ≤ b and a function with values in a normed group whose norm is bounded almost everywhere on (a, b] by K * (s - a) ^ u with -1 < u. If the function is a.e. strongly measurable on (a, b], it is interval integrable; without any measurability assumption, the norm of its integral over [a, b] is at most K * ((b - a) ^ (u + 1) / (u + 1)). Both use TauCeti.intervalIntegrable_sub_const_rpow and TauCeti.integral_sub_const_rpow. The _left forms treat the singularity at b, with bound K * (b - s) ^ u, using TauCeti.intervalIntegrable_sub_rpow and TauCeti.integral_sub_rpow.

theorem TauCeti.intervalIntegral.intervalIntegrable_of_norm_le_mul_sub_rpow_right {E : Type u_1} [NormedAddCommGroup E] {f : ℝ → E} {a b K u : ℝ} (hu : -1 < u) (hab : a ≤ b) (hmeas : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.volume.restrict (Set.Ioc a b))) (hbound : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc a b), ‖f s‖ ≤ K * (s - a) ^ u) : IntervalIntegrable f MeasureTheory.volume a b

A function whose norm is bounded almost everywhere on (a, b] by K * (s - a) ^ u with -1 < u is interval integrable on [a, b], given that it is a.e. strongly measurable there.

theorem TauCeti.intervalIntegral.norm_integral_le_of_norm_le_mul_sub_rpow_right {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {a b K u : ℝ} (hu : -1 < u) (hab : a ≤ b) (hbound : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc a b), ‖f s‖ ≤ K * (s - a) ^ u) : ‖∫ (s : ℝ) in a..b, f s‖ ≤ K * ((b - a) ^ (u + 1) / (u + 1))

A function whose norm is bounded almost everywhere on (a, b] by K * (s - a) ^ u with -1 < u has integral over [a, b] of norm at most K * ((b - a) ^ (u + 1) / (u + 1)).

theorem TauCeti.intervalIntegral.intervalIntegrable_of_norm_le_mul_sub_rpow_left {E : Type u_1} [NormedAddCommGroup E] {f : ℝ → E} {a b K u : ℝ} (hu : -1 < u) (hab : a ≤ b) (hmeas : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.volume.restrict (Set.Ioc a b))) (hbound : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc a b), ‖f s‖ ≤ K * (b - s) ^ u) : IntervalIntegrable f MeasureTheory.volume a b

The mirror image of TauCeti.intervalIntegral.intervalIntegrable_of_norm_le_mul_sub_rpow_right: the singularity is at the right endpoint b.

theorem TauCeti.intervalIntegral.norm_integral_le_of_norm_le_mul_sub_rpow_left {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {a b K u : ℝ} (hu : -1 < u) (hab : a ≤ b) (hbound : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc a b), ‖f s‖ ≤ K * (b - s) ^ u) : ‖∫ (s : ℝ) in a..b, f s‖ ≤ K * ((b - a) ^ (u + 1) / (u + 1))

The mirror image of TauCeti.intervalIntegral.norm_integral_le_of_norm_le_mul_sub_rpow_right: the singularity is at the right endpoint b.

theorem TauCeti.norm_intervalIntegral_le_of_rpow_bounds {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {f : ℝ → F} {a b A B d t : ℝ} (ha : 0 < a) (hb : 0 < b) (hA : 0 ≤ A) (hB : 0 ≤ B) (hd : 0 < d) (ht : 0 ≤ t) (hnear : ∀ᵐ (r : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 t), ‖f r‖ ≤ A * r ^ (a - 1)) (hfar : ∀ᵐ (r : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 t), ‖f r‖ ≤ B * r ^ (-b - 1)) : ‖∫ (r : ℝ) in 0..t, f r‖ ≤ A / a * d ^ a + B / b * d ^ (-b)

Integrate two complementary power bounds by splitting at d. The first power is integrable at zero and the second at infinity; the resulting bound is uniform in the endpoint t ≥ 0.

theorem TauCeti.norm_integral_le_of_ae_norm_le_rpow {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {Φ : ℝ → F} {α δ t A B : ℝ} (hα₀ : 0 < α) (hα₁ : α < 1) (ht : 0 < t) (hδ : 0 < δ) (hΦA : ∀ᵐ (s : ℝ), s ∈ Set.Ioc 0 t → ‖Φ s‖ ≤ A * (t - s) ^ ((α - 2) / 2)) (hΦB : ∀ᵐ (s : ℝ), s ∈ Set.Ioc 0 t → ‖Φ s‖ ≤ B * (t - s) ^ ((α - 3) / 2) * δ) : ‖∫ (s : ℝ) in 0..t, Φ s‖ ≤ (2 / α * A + 2 / (1 - α) * B) * δ ^ α

Splitting a singular integral at distance δ² from its singular endpoint. If the integrand is O(A (t - s)^((α - 2)/2)), which is integrable, and also O(B δ (t - s)^((α - 3)/2)), which is integrable away from s = t, then using the first bound on t - δ² < s < t and the second on 0 < s < t - δ² bounds the integral over [0, t] by (2A/α + 2B/(1 - α)) δ^α. This is the time integration behind parabolic Hölder estimates at two points at distance δ.

theorem TauCeti.norm_intervalIntegral_sub_le_of_sub_le {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] {g₁ g₂ : ℝ → V} {c β t t' D : ℝ} (hc : 0 ≤ c) (hβ₀ : 0 ≤ β) (hβ₁ : β ≤ 1) (hs₀ : 0 ≤ 2 * t' - t) (htt' : t' ≤ t) (hg₁ : IntervalIntegrable g₁ MeasureTheory.volume 0 t) (hg₂ : IntervalIntegrable g₂ MeasureTheory.volume 0 t') (hfar : ‖∫ (s : ℝ) in 0..2 * t' - t, g₁ s - g₂ s‖ ≤ D) (h₁ : ‖∫ (s : ℝ) in 2 * t' - t..t, g₁ s‖ ≤ c * (2 * (t - t')) ^ β) (h₂ : ‖∫ (s : ℝ) in 2 * t' - t..t', g₂ s‖ ≤ c * (t - t') ^ β) : ‖(∫ (s : ℝ) in 0..t, g₁ s) - ∫ (s : ℝ) in 0..t', g₂ s‖ ≤ D + 3 * c * (t - t') ^ β

Difference of two integrals over nearby intervals. Let s₀ = 2 t' - t, so that t - s₀ = 2 (t - t'), and suppose 0 ≤ s₀ ≤ t' ≤ t. If ‖∫₀^{s₀} (g₁ - g₂)‖ ≤ D, ‖∫_{s₀}^t g₁‖ ≤ c (2 (t - t')) ^ β and ‖∫_{s₀}^{t'} g₂‖ ≤ c (t - t') ^ β for 0 ≤ β ≤ 1, then ‖∫₀^t g₁ - ∫₀^{t'} g₂‖ ≤ D + 3 c (t - t') ^ β.