The barrier bound on a working interval: the limit ε ↓ 0 #
From the energy bound of CIV.ae_integral_comparisonProfile_le along the mollification radii
ε_n = 1/(n+1), the commutator term tends to zero (CIV.tendsto_integral_commutatorL2Sq) and
q_ε(·, τ) → q(·, τ) in L² of every ball (CIV.tendsto_integral_sq_mollifySlice_sub); hence
∫_{B_R} G(q(·, τ) - Ψ_σ(·, τ)) = 0 for almost every τ ∈ [τ₀, b], that is q ≤ Ψ_σ almost
everywhere on B_R, and off B_R the barrier exceeds the bound of q. This is the conclusion
q ≤ Ψ_σ of the energy argument of lem:aniso:comparison, before σ ↓ 0.
theorem
CIV.tendsto_one_div_succ_nhdsGT :
Filter.Tendsto (fun (n : ℕ) => 1 / (↑n + 1)) Filter.atTop (nhdsWithin 0 (Set.Ioi 0))
theorem
CIV.ae_ae_le_barrier_of_referenceTime
{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)
{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))
(hτ₀m : MeasureTheory.AEStronglyMeasurable (fun (y : CKN.Vec m) => q (y, τ₀)) MeasureTheory.volume)
(hτ₀M : ∀ᵐ (y : CKN.Vec m), |q (y, τ₀)| ≤ M)
(href :
∀ (n : ℕ),
(∀ᵐ (x : CKN.Vec m), ∀ᵐ (τ : ℝ) ∂MeasureTheory.volume.restrict I, mollifySlice m (1 / (↑n + 1)) q (x, τ) - mollifySlice m (1 / (↑n + 1)) q (x, τ₀) = ∫ (s : ℝ) in τ₀..τ, mollifiedRHS m d (1 / (↑n + 1)) B divB q x s) ∧ ∀ᵐ (τ : ℝ) ∂MeasureTheory.volume.restrict I, ∀ᵐ (x : CKN.Vec m), mollifySlice m (1 / (↑n + 1)) q (x, τ) - mollifySlice m (1 / (↑n + 1)) q (x, τ₀) = ∫ (s : ℝ) in τ₀..τ, mollifiedRHS m d (1 / (↑n + 1)) B divB q x s)
:
The barrier bound on a working interval, from a reference time τ₀.