The comparison energy on a working interval #
The assembled Grönwall bound of CIV.Comparison.Direct.EnergyGronwall on a working interval
[τ₀, b] ⊆ I: see that module's docstring for the statement and the route.
theorem
CIV.ae_integral_comparisonProfile_le
{m d : ℕ}
{I : Set ℝ}
(hI : IsOpen I)
(hIoc : I.OrdConnected)
{B : CKN.Vec m × ℝ → CKN.Vec m}
{divB q : CKN.Vec m × ℝ → ℝ}
(hB : IsAdmissibleDrift m I B divB)
(hq : IsLocallyBoundedOn m I q)
(heq : IsDistributionalDriftDiffusion m d I B divB q)
{ε : ℝ}
(hε : 0 < ε)
{M σ Mq τ₀ b : ℝ}
{Λ : NNReal}
(hσ : 0 < σ)
(hM : 0 ≤ M)
(hMq : 0 ≤ Mq)
(hτ₀b : τ₀ ≤ b)
(hsub : Set.Icc τ₀ b ⊆ I)
(hgood :
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Icc τ₀ b), MeasureTheory.AEStronglyMeasurable (fun (y : CKN.Vec m) => q (y, s)) MeasureTheory.volume ∧ (∀ᵐ (y : CKN.Vec m), |q (y, s)| ≤ Mq) ∧ (∀ (x : CKN.Vec m), ‖B (x, s)‖ ≤ ↑Λ) ∧ (LipschitzWith Λ fun (x : CKN.Vec m) => B (x, s)) ∧ (∀ (x : CKN.Vec m), |divB (x, s)| ≤ ↑Λ) ∧ ∀ (ψ : CKN.Vec m → ℝ),
ContDiff ℝ (↑⊤) ψ →
HasCompactSupport ψ →
∫ (x : CKN.Vec m), divB (x, s) * ψ x = -∫ (x : CKN.Vec m), ∑ i : Fin m, B (x, s) i * (fderiv ℝ ψ x) (CKN.basisVec i))
(hq0 : ∀ (x : CKN.Vec m), mollifySlice m ε q (x, τ₀) ≤ M)
(hA1 :
∀ᵐ (x : CKN.Vec m), ∀ᵐ (τ : ℝ) ∂MeasureTheory.volume.restrict I, mollifySlice m ε q (x, τ) - mollifySlice m ε q (x, τ₀) = ∫ (s : ℝ) in τ₀..τ, mollifiedRHS m d ε B divB q x s)
(hA2 :
∀ᵐ (τ : ℝ) ∂MeasureTheory.volume.restrict I, ∀ᵐ (x : CKN.Vec m), mollifySlice m ε q (x, τ) - mollifySlice m ε q (x, τ₀) = ∫ (s : ℝ) in τ₀..τ, mollifiedRHS m d ε B divB q x s)
:
∀ᵐ (τ : ℝ) ∂MeasureTheory.volume.restrict (Set.Icc τ₀ b), ∀ (δ : ℝ),
0 < δ →
∫ (x : CKN.Vec m), comparisonProfile (mollifySlice m ε q (x, τ) - barrier m M σ (barrierRate m d ↑Λ) τ₀ (x, τ)) ≤ (δ * (MeasureTheory.volume (Metric.closedBall 0 (Mq / σ))).toReal * (b - τ₀) + 1 / (4 * δ) * ∫ (s : ℝ) in τ₀..b, commutatorL2Sq m ε (Mq / σ) B divB q s) * Real.exp (↑Λ * (b - τ₀))
The comparison energy bound at fixed ε and σ (eq:aniso:comparison:positive:energy
followed by Grönwall's inequality).