Documentation

LeanPool.AnomalousDiffusion.AVenhance.Infra.Section5.RelativeError.LeadingErrorBoundsL2Ioi

LΒ²((0,1)×𝕋²) bookkeeping with regularity only on the open half space #

LeadingErrorBoundsL2 integrates functions continuous on [0,∞) Γ— ℝ² over the time cell. The field βˆ‡HTilde_m is only known to be continuous on (0,∞) Γ— ℝ² (at t = 0 it sees the arbitrary negative-time extension of T), so here the dominating function is split as B + |βˆ‡HTilde_m| with B continuous on [0,∞) Γ— ℝ² and the βˆ‡HTilde_m part only continuous on the open half space. If the error field is square integrable then so is βˆ‡HTilde_m; if it is not, the Bochner integral defining its norm vanishes.

source
theorem AVenhance.Infra.Section5.RelativeError.abs_apply_le_sqrt_vecNormSq (v : Homogenization.Vec 2) (i : Fin 2) :
|v i| ≀ √(Homogenization.vecNormSq v)
source
theorem AVenhance.Infra.Section5.RelativeError.continuousOn_sqrt_vecNormSq {s : Set (ℝ Γ— Homogenization.Vec 2)} {V : ℝ Γ— Homogenization.Vec 2 β†’ Homogenization.Vec 2} (h : βˆ€ (i : Fin 2), ContinuousOn (fun (p : ℝ Γ— Homogenization.Vec 2) => V p i) s) :
ContinuousOn (fun (p : ℝ Γ— Homogenization.Vec 2) => √(Homogenization.vecNormSq (V p))) s
source
theorem AVenhance.Infra.Section5.RelativeError.integral_sqrt_vecNormSq_sq (V : ℝ β†’ Homogenization.Vec 2 β†’ Homogenization.Vec 2) :
∫ (p : ℝ Γ— Homogenization.Vec 2) in timeCube, √(Homogenization.vecNormSq (V p.1 p.2)) ^ 2 = spaceTimeGradNormSq V
source
theorem AVenhance.Infra.Section5.RelativeError.aestronglyMeasurable_timeCube_of_continuousOn_Ioi {f : ℝ Γ— Homogenization.Vec 2 β†’ ℝ} (hf : ContinuousOn f (Set.Ioi 0 Γ—Λ’ Set.univ)) :
MeasureTheory.AEStronglyMeasurable f (MeasureTheory.volume.restrict timeCube)

Functions continuous on the open half space are a.e. strongly measurable on the time cell.

source
theorem AVenhance.Infra.Section5.RelativeError.LeadingErrorBoundsL2Ioi.vecNormSq_embed' (a : ℝ) :
Homogenization.vecNormSq ![a, 0] = a ^ 2
source
theorem AVenhance.Infra.Section5.RelativeError.LeadingErrorBoundsL2Ioi.embed_add' (a b : ℝ) :
![a, 0] + ![b, 0] = ![a + b, 0]
source
theorem AVenhance.Infra.Section5.RelativeError.sqrt_setIntegral_sq_add_le_of_integrable {f g : ℝ Γ— Homogenization.Vec 2 β†’ ℝ} (hfm : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.volume.restrict timeCube)) (hgm : MeasureTheory.AEStronglyMeasurable g (MeasureTheory.volume.restrict timeCube)) (hf : MeasureTheory.Integrable (fun (p : ℝ Γ— Homogenization.Vec 2) => f p ^ 2) (MeasureTheory.volume.restrict timeCube)) (hg : MeasureTheory.Integrable (fun (p : ℝ Γ— Homogenization.Vec 2) => g p ^ 2) (MeasureTheory.volume.restrict timeCube)) :
√(∫ (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 for square-integrable functions.

source
theorem AVenhance.Infra.Section5.RelativeError.sqrt_setIntegral_sq_three_le {f₁ fβ‚‚ f₃ : ℝ Γ— Homogenization.Vec 2 β†’ ℝ} {c₁ cβ‚‚ c₃ : ℝ} (hc₁ : 0 ≀ c₁) (hcβ‚‚ : 0 ≀ cβ‚‚) (hc₃ : 0 ≀ c₃) (h₁ : ContinuousOn f₁ (Set.Ici 0 Γ—Λ’ Set.univ)) (hβ‚‚ : ContinuousOn fβ‚‚ (Set.Ici 0 Γ—Λ’ Set.univ)) (h₃ : ContinuousOn f₃ (Set.Ici 0 Γ—Λ’ Set.univ)) :
√(∫ (p : ℝ Γ— Homogenization.Vec 2) in timeCube, (c₁ * f₁ p + cβ‚‚ * fβ‚‚ p + c₃ * f₃ p) ^ 2) ≀ c₁ * √(∫ (p : ℝ Γ— Homogenization.Vec 2) in timeCube, f₁ p ^ 2) + cβ‚‚ * √(∫ (p : ℝ Γ— Homogenization.Vec 2) in timeCube, fβ‚‚ p ^ 2) + c₃ * √(∫ (p : ℝ Γ— Homogenization.Vec 2) in timeCube, f₃ p ^ 2)

LΒ² triangle inequality for a weighted sum of three functions continuous on the closed half space.

source
theorem AVenhance.Infra.Section5.RelativeError.sqrt_spaceTimeGradNormSq_le_of_sub_component_le {F G : ℝ β†’ Homogenization.Vec 2 β†’ Homogenization.Vec 2} {B : ℝ Γ— Homogenization.Vec 2 β†’ ℝ} (hB : ContinuousOn B (Set.Ici 0 Γ—Λ’ Set.univ)) (hG : βˆ€ (i : Fin 2), ContinuousOn (fun (p : ℝ Γ— Homogenization.Vec 2) => G p.1 p.2 i) (Set.Ioi 0 Γ—Λ’ Set.univ)) (hF : βˆ€ t ∈ Set.Ioo 0 1, βˆ€ (x : Homogenization.Vec 2) (i : Fin 2), |F t x i - G t x i| ≀ B (t, x)) :
√(spaceTimeGradNormSq F) ≀ 2 * (√(∫ (p : ℝ Γ— Homogenization.Vec 2) in timeCube, B p ^ 2) + √(spaceTimeGradNormSq G))

If F - G is componentwise dominated by B, continuous on the closed half space, and every component of G is continuous on the open half space, then β€–Fβ€–_{LΒ²} ≀ 2 (β€–Bβ€–_{LΒ²} + β€–Gβ€–_{LΒ²}).