Documentation

LeanPool.AnomalousDiffusion.AVenhance.Infra.Section5.RelativeError.LeadingErrorBoundsL2

L²((0,1)×𝕋²) bookkeeping for the leading-error estimate #

Elementary measure-theoretic facts used to turn pointwise bounds on the remainder fields of e.grad.tildetheta.again into spaceTimeGradNormSq bounds: integrability of functions continuous on [0,∞) × ℝ² over the time cell, the scalar L² triangle inequality, and the comparison ‖F‖_{L²} ≤ 2 ‖B‖_{L²} when every component of F is dominated by a continuous B.

source
def AVenhance.Infra.Section5.RelativeError.LeadingErrorBoundsL2.closedTimeCell :
Set (ℝ × Homogenization.Vec 2)

Compact closure of the time cell.

Equations
Instances For
    source
    theorem AVenhance.Infra.Section5.RelativeError.LeadingErrorBoundsL2.isCompact_closedTimeCell :
    IsCompact closedTimeCell
    source
    theorem AVenhance.Infra.Section5.RelativeError.LeadingErrorBoundsL2.timeCube_subset_closedTimeCell :
    timeCube ⊆ closedTimeCell
    source
    theorem AVenhance.Infra.Section5.RelativeError.LeadingErrorBoundsL2.closedTimeCell_subset :
    closedTimeCell ⊆ Set.Ici 0 ×ˢ Set.univ
    source
    theorem AVenhance.Infra.Section5.RelativeError.integrable_timeCube_of_continuousOn {f : ℝ × Homogenization.Vec 2 → ℝ} (hf : ContinuousOn f (Set.Ici 0 ×ˢ Set.univ)) :
    MeasureTheory.Integrable f (MeasureTheory.volume.restrict timeCube)

    Functions continuous on [0,∞) × ℝ² are integrable on the time cell.

    source
    theorem AVenhance.Infra.Section5.RelativeError.measurableSet_timeCube :
    MeasurableSet timeCube
    source
    theorem AVenhance.Infra.Section5.RelativeError.vecNormSq_nonneg_of_vec2 (v : Homogenization.Vec 2) :
    0 ≤ Homogenization.vecNormSq v
    source
    theorem AVenhance.Infra.Section5.RelativeError.LeadingErrorBoundsL2.vecNormSq_embed (a : ℝ) :
    Homogenization.vecNormSq ![a, 0] = a ^ 2
    source
    theorem AVenhance.Infra.Section5.RelativeError.LeadingErrorBoundsL2.embed_add (a b : ℝ) :
    ![a, 0] + ![b, 0] = ![a + b, 0]
    source
    theorem AVenhance.Infra.Section5.RelativeError.sqrt_setIntegral_sq_add_le {f g : ℝ × Homogenization.Vec 2 → ℝ} (hf : ContinuousOn f (Set.Ici 0 ×ˢ Set.univ)) (hg : ContinuousOn g (Set.Ici 0 ×ˢ Set.univ)) :
    √(∫ (p : ℝ × Homogenization.Vec 2) in timeCube, (f p + g p) ^ 2) ≤ √(∫ (p : ℝ × Homogenization.Vec 2) in timeCube, f p ^ 2) + √(∫ (p : ℝ × Homogenization.Vec 2) in timeCube, g p ^ 2)

    Scalar L² triangle inequality on the time cell.

    source
    theorem AVenhance.Infra.Section5.RelativeError.sqrt_setIntegral_sq_const_mul {c : ℝ} (hc : 0 ≤ c) (f : ℝ × Homogenization.Vec 2 → ℝ) :
    √(∫ (p : ℝ × Homogenization.Vec 2) in timeCube, (c * f p) ^ 2) = c * √(∫ (p : ℝ × Homogenization.Vec 2) in timeCube, f p ^ 2)