Positive source primitives from genuine spacetime L2 control. Neither source traces at zero nor pointwise-in-time source estimates are needed.

def AVenhance.Infra.Section5.RelativeError.RelativeInitialDefectSourceIntegral.sourceClosedCube : Set (Homogenization.Vec 2)

Closed spatial unit cell used for compactness and periodic integration.

Equations

• AVenhance.Infra.Section5.RelativeError.RelativeInitialDefectSourceIntegral.sourceClosedCube = Set.univ.pi fun (x : Fin 2) => Set.Icc 0 1

theorem AVenhance.Infra.Section5.RelativeError.RelativeInitialDefectSourceIntegral.sourceClosedCube_compact : IsCompact sourceClosedCube

theorem AVenhance.Infra.Section5.RelativeError.RelativeInitialDefectSourceIntegral.sourceCube_ae_eq : unitCube =ᵐ[MeasureTheory.volume] sourceClosedCube

instance AVenhance.Infra.Section5.RelativeError.RelativeInitialDefectSourceIntegral.sourceWindow_locallyCompact (a b : ℝ) : LocallyCompactSpace { t : ℝ // t ∈ Set.Icc a b }

theorem AVenhance.Infra.Section5.RelativeError.relative_initial_source_norm_continuous_pos {f : ℝ → Homogenization.Vec 2 → ℝ} (hf : ContinuousOn (fun (z : ℝ × Homogenization.Vec 2) => f z.1 z.2) (Set.Ioi 0 ×ˢ Set.univ)) {a b : ℝ} (ha : 0 < a) : ContinuousOn (fun (t : ℝ) => √(l2NormSq (f t))) (Set.Icc a b)

Positive joint continuity gives continuity of the spatial L2 norm on each positive compact window.

theorem AVenhance.Infra.Section5.RelativeError.relative_initial_source_integral_of_eLpNorm {f : ℝ → Homogenization.Vec 2 → ℝ} (hf : ContinuousOn (fun (z : ℝ × Homogenization.Vec 2) => f z.1 z.2) (Set.Ioi 0 ×ˢ Set.univ)) {B a b : ℝ} (hB : 0 ≤ B) (ha : 0 < a) (hab : a ≤ b) (hb : b < 1) (hbound : MeasureTheory.eLpNorm (fun (z : ℝ × Homogenization.Vec 2) => f z.1 z.2) 2 (MeasureTheory.volume.restrict timeCube) ≤ ENNReal.ofReal B) : ∫ (t : ℝ) in a..b, √(l2NormSq (f t)) ≤ √b * B

The endpoint source L2 bound controls its primitive uniformly as the left endpoint tends to zero through positive times.