Generic torus transport energy, isolated from the broken physical Hm consumer. The valid generic argument is ported from HmTransportedEnergy; no physical source estimate is inferred from these analytic lemmas.

def AVenhance.Infra.Section5.RelativeError.Transport.RelativeInitialDefectTransport.hmEnergyClosedCube : Set (Homogenization.Vec 2)

Closed spatial unit cell used for compactness and periodic integration.

Equations

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

theorem AVenhance.Infra.Section5.RelativeError.Transport.RelativeInitialDefectTransport.hmEnergyClosedCube_compact : IsCompact hmEnergyClosedCube

theorem AVenhance.Infra.Section5.RelativeError.Transport.RelativeInitialDefectTransport.hmEnergy_unitCube_ae_eq_closedCube : unitCube =ᵐ[MeasureTheory.volume] hmEnergyClosedCube

theorem AVenhance.Infra.Section5.RelativeError.Transport.RelativeInitialDefectTransport.hmEnergy_cellAverage_eq_unitCube (f : Homogenization.Vec 2 → ℝ) : Ergodic.cellAverage f = ∫ (x : Homogenization.Vec 2) in unitCube, f x

instance AVenhance.Infra.Section5.RelativeError.Transport.RelativeInitialDefectTransport.hmEnergy_uIcc_locallyCompact (a b : ℝ) : LocallyCompactSpace { x : ℝ // x ∈ Set.uIcc a b }

theorem AVenhance.Infra.Section5.RelativeError.Transport.RelativeInitialDefectTransport.hmEnergy_slice_continuous {g : ℝ × Homogenization.Vec 2 → ℝ} (hg : ContinuousOn g (Set.Ioi 0 ×ˢ Set.univ)) {s : ℝ} (hs : 0 < s) : Continuous fun (x : Homogenization.Vec 2) => g (s, x)

theorem AVenhance.Infra.Section5.RelativeError.Transport.RelativeInitialDefectTransport.hmEnergy_comp_integral_eq {F : ℝ → Homogenization.Vec 2 → ℝ} (X : ℝ → Ergodic.PeriodicVolumePreservingDiffeomorphism 2) (hFper : ∀ (t : ℝ), IsZ2Periodic (F t)) (t : ℝ) : ∫ (x : Homogenization.Vec 2) in unitCube, F t ((X t).toFun x) ^ 2 = l2NormSq (F t)

The squared spatial norm is unchanged by a periodic volume-preserving diffeomorphism of the flow.

theorem AVenhance.Infra.Section5.RelativeError.Transport.hm_transported_norm_continuous_of_joint {F : ℝ → Homogenization.Vec 2 → ℝ} (X : ℝ → Ergodic.PeriodicVolumePreservingDiffeomorphism 2) (hFper : ∀ (t : ℝ), IsZ2Periodic (F t)) (hComp : ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => F p.1 ((X p.1).toFun p.2)) (Set.Ioi 0 ×ˢ Set.univ)) {a b : ℝ} (ha : 0 < a) : ContinuousOn (fun (t : ℝ) => √(l2NormSq (F t))) (Set.Icc a b)

Joint continuity along a periodic measure-preserving flow makes the spatial L² norm continuous in time on every compact interval bounded away from zero.

theorem AVenhance.Infra.Section5.RelativeError.Transport.hm_transported_energy_ftc_integrated {F source : ℝ → Homogenization.Vec 2 → ℝ} (X : ℝ → Ergodic.PeriodicVolumePreservingDiffeomorphism 2) (hFper : ∀ (t : ℝ), IsZ2Periodic (F t)) (hSourcePer : ∀ (t : ℝ), IsZ2Periodic (source t)) (hComp : ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => F p.1 ((X p.1).toFun p.2)) (Set.Ioi 0 ×ˢ Set.univ)) (hSourceComp : ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => source p.1 ((X p.1).toFun p.2)) (Set.Ioi 0 ×ˢ Set.univ)) (hMaterial : ∀ (t : ℝ), 0 < t → ∀ (x : Homogenization.Vec 2), HasDerivAt (fun (s : ℝ) => F s ((X s).toFun x)) (source t ((X t).toFun x)) t) {a t H D : ℝ} (ha : 0 < a) (ht : 0 < t) (hH : 0 ≤ H) (hzero : F a = 0) (hFbound : ∀ s ∈ Set.uIcc a t, √(l2NormSq (F s)) ≤ H) (hSourceIntegral : |∫ (s : ℝ) in a..t, √(l2NormSq (source s))| ≤ D) : √(l2NormSq (F t)) ^ 2 ≤ 2 * D * H

A transported field with zero data at the left end of an interval satisfies the standard energy FTC bound. source is its actual material derivative. The proof uses torus volume preservation, Cauchy--Schwarz, and FTC; H and D are abstract amplitudes and do not mention theta₀ or a time supremum of the underlying solution.

theorem AVenhance.Infra.Section5.RelativeError.Transport.hm_transport_cell_sup_le_of_continuous {f : ℝ → ℝ} {cell : Set ℝ} {H L D : ℝ} (hnonneg : ∀ t ∈ cell, 0 ≤ f t) (hLD : 0 ≤ L * D) (hFTC : ∀ t ∈ cell, f t ^ 2 ≤ 2 * L * D * H) (hH : ∃ t₀ ∈ cell, H = f t₀ ∧ ∀ t ∈ cell, f t ≤ f t₀) (t : ℝ) : t ∈ cell → f t ≤ 2 * L * D

A maximum on a compact interval replaces the separate time-uniform norm and attainment premises in the transport absorption argument.