Time assembly for the tiny source contract #
Abstract measure-theoretic step: if the slices of the negative norm are dominated by a divergence
part √‖F‖² (with ‖F‖² ≤ 2‖d‖² + 2‖e‖²) and a nondivergence part (2π)⁻¹ √‖n‖², if the
d-energy is controlled in L²_t by the contract and the remaining energy
4‖e‖² + 2 (2π)⁻² ‖n‖² by its lower integral, then the time negative norm is bounded by
2 b_d + √S.
theorem
AVenhance.Infra.Section5.Contracts.sc_sq_le_of_slices
{X : ENNReal}
{GF Gd Ge N : ℝ}
(hGd : 0 ≤ Gd)
(hGe : 0 ≤ Ge)
(hN : 0 ≤ N)
(hGF0 : 0 ≤ GF)
(hGF : GF ≤ 2 * Gd + 2 * Ge)
(hX : X ≤ ENNReal.ofReal √GF + ENNReal.ofReal ((2 * Real.pi)⁻¹ * √N))
:
The pointwise-in-time estimate X² ≤ ofReal (4 Gd) + ofReal (4 Ge + 2 (2π)⁻² N).
theorem
AVenhance.Infra.Section5.Contracts.sc_time_norm_le
{X : ℝ → ENNReal}
{GF Gd Ge N : ℝ → ℝ}
{bd S : ℝ}
(hbd : 0 ≤ bd)
(hS : 0 ≤ S)
(hGd : ∀ t ∈ Set.Ioo 0 1, 0 ≤ Gd t)
(hGe : ∀ t ∈ Set.Ioo 0 1, 0 ≤ Ge t)
(hN : ∀ t ∈ Set.Ioo 0 1, 0 ≤ N t)
(hGF0 : ∀ t ∈ Set.Ioo 0 1, 0 ≤ GF t)
(hGF : ∀ t ∈ Set.Ioo 0 1, GF t ≤ 2 * Gd t + 2 * Ge t)
(hX : ∀ t ∈ Set.Ioo 0 1, X t ≤ ENNReal.ofReal √(GF t) + ENNReal.ofReal ((2 * Real.pi)⁻¹ * √(N t)))
(hmeas : AEMeasurable (fun (t : ℝ) => ENNReal.ofReal (Gd t)) (MeasureTheory.volume.restrict (Set.Ioo 0 1)))
(hd : (∫⁻ (t : ℝ) in Set.Ioo 0 1, ENNReal.ofReal √(Gd t) ^ 2) ^ (1 / 2) ≤ ENNReal.ofReal bd)
(hrest : ∫⁻ (t : ℝ) in Set.Ioo 0 1, ENNReal.ofReal (4 * Ge t + 2 * (2 * Real.pi)⁻¹ ^ 2 * N t) ≤ ENNReal.ofReal S)
:
Time assembly.