Assembly of lem:aniso:comparison

On each compact working interval [a, b] ⊆ I the drift is bounded and Lipschitz with one constant Λ and q is bounded by one constant; for almost every τ₀ ∈ [a, b] which is a reference time of the mollified equation for every radius 1/(n+1), the barrier bound q ≤ Ψ_σ of CIV.ae_ae_le_barrier_of_referenceTime holds on [τ₀, b] for every σ > 0, and σ ↓ 0 gives q ≤ ‖q(·, τ₀)‖_{L^∞} there. Countably many rational working intervals exhaust I, the same argument for -q gives the two-sided bound, and the essential supremum bridge turns it into eq:aniso:comparison:conclusion.

theorem CIV.ae_ae_le_of_window {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) {a b : ℝ} (hab : Set.Icc a b ⊆ I) : ∀ᵐ (τ₀ : ℝ) ∂MeasureTheory.volume.restrict I, τ₀ ∈ Set.Icc a b → ∀ (M : ℝ), 0 ≤ M → (∀ᵐ (x : CKN.Vec m), |q (x, τ₀)| ≤ M) → ∀ᵐ (τ : ℝ) ∂MeasureTheory.volume.restrict (Set.Icc τ₀ b), ∀ᵐ (x : CKN.Vec m), q (x, τ) ≤ M

The upper bound on one working interval. For almost every τ₀ ∈ [a, b], every nonnegative essential bound M of q(·, τ₀) bounds q from above at almost every time of [τ₀, b].

theorem CIV.ae_ae_le_of_isDistributionalDriftDiffusion {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) : ∀ᵐ (τ₀ : ℝ) ∂MeasureTheory.volume.restrict I, ∀ (M : ℝ), 0 ≤ M → (∀ᵐ (x : CKN.Vec m), |q (x, τ₀)| ≤ M) → ∀ᵐ (τ : ℝ) ∂MeasureTheory.volume.restrict I, τ₀ < τ → ∀ᵐ (x : CKN.Vec m), q (x, τ) ≤ M

The upper bound on I. For almost every τ₀ ∈ I, every nonnegative essential bound of q(·, τ₀) bounds q from above at almost every later time of I.

theorem CIV.ae_ae_abs_le_of_isDistributionalDriftDiffusion {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) : ∀ᵐ (τ₀ : ℝ) (τ : ℝ) ∂MeasureTheory.volume.restrict I, τ₀ < τ → ∀ (M : ℝ), (∀ᵐ (x : CKN.Vec m), |q (x, τ₀)| ≤ M) → ∀ᵐ (x : CKN.Vec m), |q (x, τ)| ≤ M

The two-sided transfer of essential bounds. For almost every τ₀ ∈ I and almost every later τ ∈ I, every essential bound of |q(·, τ₀)| is an essential bound of |q(·, τ)|. The canonical bound ‖q(·, τ₀)‖_{L^∞} is used for q and for -q, so that the exceptional set of times does not depend on the bound.

theorem CIV.comparison_of_isDistributionalDriftDiffusion {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) : ∀ᵐ (τ₀ : ℝ) (τ : ℝ) ∂MeasureTheory.volume.restrict I, τ₀ < τ → MeasureTheory.eLpNorm (fun (x : CKN.Vec m) => q (x, τ)) ⊤ MeasureTheory.volume ≤ MeasureTheory.eLpNorm (fun (x : CKN.Vec m) => q (x, τ₀)) ⊤ MeasureTheory.volume

lem:aniso:comparison, first assertion (eq:aniso:comparison:conclusion).