A transported energy estimate on the unit torus. The flow and material derivative are explicit inputs, so the lemma is independent of the amplitude normalization used to bound the source.

theorem AVenhance.Infra.Section4.HmTransportedEnergy.hmEnergy_stDiv_eq_vecDiv {F : Section5.ST → Homogenization.Vec 2} {t : ℝ} {x : Homogenization.Vec 2} (hF : DifferentiableAt ℝ F (t, x)) : Section5.stDiv F (t, x) = vecDiv (fun (y : Homogenization.Vec 2) => F (t, y)) x

def AVenhance.Infra.Section4.HmTransportedEnergy.hmEnergyClosedCube : Set (Homogenization.Vec 2)

Closed spatial unit cell used for compactness and periodic integration.

Equations

• AVenhance.Infra.Section4.HmTransportedEnergy.hmEnergyClosedCube = Set.univ.pi fun (x : Fin 2) => Set.Icc 0 1

theorem AVenhance.Infra.Section4.HmTransportedEnergy.hmEnergyClosedCube_compact : IsCompact hmEnergyClosedCube

theorem AVenhance.Infra.Section4.HmTransportedEnergy.hmEnergy_unitCube_ae_eq_closedCube : unitCube =ᵐ[MeasureTheory.volume] hmEnergyClosedCube

theorem AVenhance.Infra.Section4.HmTransportedEnergy.hmEnergy_cellAverage_eq_unitCube (f : Homogenization.Vec 2 → ℝ) : Ergodic.cellAverage f = ∫ (x : Homogenization.Vec 2) in unitCube, f x

instance AVenhance.Infra.Section4.HmTransportedEnergy.hmEnergy_uIcc_locallyCompact (a b : ℝ) : LocallyCompactSpace { x : ℝ // x ∈ Set.uIcc a b }

theorem AVenhance.Infra.Section4.HmTransportedEnergy.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.Section4.hm_periodic_divergence_pairing {f : Homogenization.Vec 2 → ℝ} {V : Homogenization.Vec 2 → Homogenization.Vec 2} (hf : ContDiff ℝ 1 f) (hV : ContDiff ℝ 1 V) (hfper : IsZ2Periodic f) (hVper : ∀ (i : Fin 2), IsZ2Periodic fun (x : Homogenization.Vec 2) => V x i) : ∫ (x : Homogenization.Vec 2) in unitCube, f x * vecDiv V x = -∫ (x : Homogenization.Vec 2) in unitCube, spaceGrad f x 0 * V x 0 + spaceGrad f x 1 * V x 1

The divergence in the material equation acts on H_m through the periodic flux pairing. This identity avoids asking for a scalar L²_x bound on div d; it is the form needed to combine d with the space-time gradient estimate.

theorem AVenhance.Infra.Section4.hm_periodic_source_pairing {f g : Homogenization.Vec 2 → ℝ} {V : Homogenization.Vec 2 → Homogenization.Vec 2} (hf : ContDiff ℝ 1 f) (hg : Continuous g) (hV : ContDiff ℝ 1 V) (hfper : IsZ2Periodic f) (hVper : ∀ (i : Fin 2), IsZ2Periodic fun (x : Homogenization.Vec 2) => V x i) : ∫ (x : Homogenization.Vec 2) in unitCube, f x * (g x + vecDiv V x) = (∫ (x : Homogenization.Vec 2) in unitCube, f x * g x) - ∫ (x : Homogenization.Vec 2) in unitCube, spaceGrad f x 0 * V x 0 + spaceGrad f x 1 * V x 1

The scalar material source paired against H_m splits into its regular source term and the dual pairing with its vector flux remainder.

theorem AVenhance.Infra.Section4.HmTransportedEnergy.hmEnergy_comp_integral_eq_at {F : ℝ → Homogenization.Vec 2 → ℝ} (X : ℝ → Ergodic.PeriodicVolumePreservingDiffeomorphism 2) {t : ℝ} (hFper : IsZ2Periodic (F 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.Section4.HmTransportedEnergy.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)

noncomputable def AVenhance.Infra.Section4.hmRegularPairing {F G : ℝ → Homogenization.Vec 2 → ℝ} (t : ℝ) : ℝ

The regular scalar source paired with a field.

Equations

• AVenhance.Infra.Section4.hmRegularPairing t = ∫ (x : Homogenization.Vec 2) in AVenhance.unitCube, F t x * G t x

noncomputable def AVenhance.Infra.Section4.hmFluxPairing {F : ℝ → Homogenization.Vec 2 → ℝ} {V : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (t : ℝ) : ℝ

The signed torus pairing of the gradient with its vector flux.

Equations

• AVenhance.Infra.Section4.hmFluxPairing t = -∫ (x : Homogenization.Vec 2) in AVenhance.unitCube, AVenhance.spaceGrad (F t) x 0 * V t x 0 + AVenhance.spaceGrad (F t) x 1 * V t x 1

theorem AVenhance.Infra.Section4.hm_transported_energy_derivative_of_pairing {F G source : ℝ → Homogenization.Vec 2 → ℝ} {V : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (X : ℝ → Ergodic.PeriodicVolumePreservingDiffeomorphism 2) (hFper : ∀ (t : ℝ), 0 < t → IsZ2Periodic (F t)) (hSourcePer : ∀ (t : ℝ), 0 < t → IsZ2Periodic (source t)) (hVper : ∀ (t : ℝ), 0 < t → ∀ (i : Fin 2), IsZ2Periodic fun (x : Homogenization.Vec 2) => V t x i) (hF : ∀ (t : ℝ), 0 < t → ContDiff ℝ 1 (F t)) (hG : ∀ (t : ℝ), 0 < t → Continuous (G t)) (hV : ∀ (t : ℝ), 0 < t → ContDiff ℝ 1 (V 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)) (hSourceSplit : ∀ (t : ℝ) (x : Homogenization.Vec 2), source t x = G t x + vecDiv (V t) x) (hMaterial : ∀ (t : ℝ), 0 < t → ∀ (x : Homogenization.Vec 2), HasDerivAt (fun (s : ℝ) => F s ((X s).toFun x)) (source t ((X t).toFun x)) t) {t : ℝ} (ht : 0 < t) : HasDerivAt (fun (s : ℝ) => l2NormSq (F s)) (2 * (hmRegularPairing t + hmFluxPairing t)) t

Along a volume-preserving flow, the actual material derivative G + div V differentiates the transported squared norm by the regular pairing plus the integrated gradient-flux pairing. No scalar L² estimate on div V is used.

theorem AVenhance.Infra.Section4.hm_transported_norm_continuous_of_joint {F : ℝ → Homogenization.Vec 2 → ℝ} (X : ℝ → Ergodic.PeriodicVolumePreservingDiffeomorphism 2) (hFper : ∀ (t : ℝ), 0 < 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.Section4.hm_transported_energy_ftc {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) (hSourceBound : ∀ s ∈ Set.uIcc a t, √(l2NormSq (source s)) ≤ D) : √(l2NormSq (F t)) ^ 2 ≤ 2 * |t - a| * 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.Section4.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.

theorem AVenhance.Infra.Section4.hm_transported_energy_uniform {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 b D : ℝ} (ha : 0 < a) (hab : a ≤ b) (hD : 0 ≤ D) (hzero : F a = 0) (hNormCont : ContinuousOn (fun (t : ℝ) => √(l2NormSq (F t))) (Set.Icc a b)) (hSourceBound : ∀ s ∈ Set.Icc a b, √(l2NormSq (source s)) ≤ D) (t : ℝ) : t ∈ Set.Icc a b → √(l2NormSq (F t)) ≤ 2 * (b - a) * D

Uniform-in-time version of the transported energy estimate. The maximum is taken internally on the compact interval, while D and the field scale remain abstract parameters.

theorem AVenhance.Infra.Section4.hm_transport_cell_sup_le_of_quadraticCoefficients {f : ℝ → ℝ} {cell : Set ℝ} {H A B : ℝ} (hnonneg : ∀ t ∈ cell, 0 ≤ f t) (hA : 0 ≤ A) (hB : 0 ≤ B) (hFTC : ∀ t ∈ cell, f t ^ 2 ≤ A * H + B) (hmax : ∃ t₀ ∈ cell, H = f t₀ ∧ ∀ t ∈ cell, f t ≤ f t₀) (t : ℝ) : t ∈ cell → f t ≤ A + √B

Maximum absorption for an inequality f² ≤ A H + B, with nonnegative coefficients.

theorem AVenhance.Infra.Section4.hm_energy_ftc_of_integrated_pairings {energy regular flux : ℝ → ℝ} {a t L G H Q : ℝ} (hderiv : ∀ s ∈ Set.uIcc a t, HasDerivAt energy (2 * (regular s + flux s)) s) (hregInt : IntervalIntegrable regular MeasureTheory.volume a t) (hfluxInt : IntervalIntegrable flux MeasureTheory.volume a t) (hzero : energy a = 0) (hregBound : |∫ (s : ℝ) in a..t, regular s| ≤ √L * G * H) (hfluxBound : |∫ (s : ℝ) in a..t, flux s| ≤ Q) : energy t ≤ 2 * (√L * G * H + Q)

FTC for a transported energy after the spatial integration by parts has split its derivative into the regular pairing and the flux pairing. The two integrated bounds stay separate: the first carries the factor H absorbed by the cell maximum, while the flux contribution is additive.

theorem AVenhance.Infra.Section4.hm_transported_norm_uniform_of_integrated_pairings {F G source : ℝ → Homogenization.Vec 2 → ℝ} {V : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (X : ℝ → Ergodic.PeriodicVolumePreservingDiffeomorphism 2) (hFper : ∀ (t : ℝ), 0 < t → IsZ2Periodic (F t)) (hSourcePer : ∀ (t : ℝ), 0 < t → IsZ2Periodic (source t)) (hVper : ∀ (t : ℝ), 0 < t → ∀ (i : Fin 2), IsZ2Periodic fun (x : Homogenization.Vec 2) => V t x i) (hF : ∀ (t : ℝ), 0 < t → ContDiff ℝ 1 (F t)) (hG : ∀ (t : ℝ), 0 < t → Continuous (G t)) (hV : ∀ (t : ℝ), 0 < t → ContDiff ℝ 1 (V 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)) (hSourceSplit : ∀ (t : ℝ) (x : Homogenization.Vec 2), source t x = G t x + vecDiv (V t) x) (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 b anchor Gscale Q : ℝ} (ha : 0 < a) (hab : a ≤ b) (hanchor : anchor ∈ Set.Icc a b) (hzero : F anchor = fun (x : Homogenization.Vec 2) => 0) (hNormCont : ContinuousOn (fun (t : ℝ) => √(l2NormSq (F t))) (Set.Icc a b)) (hGscale : 0 ≤ Gscale) (hQ : 0 ≤ Q) (hregInt : ∀ t ∈ Set.Icc a b, IntervalIntegrable hmRegularPairing MeasureTheory.volume anchor t) (hfluxInt : ∀ t ∈ Set.Icc a b, IntervalIntegrable hmFluxPairing MeasureTheory.volume anchor t) (hregBound : ∀ t ∈ Set.Icc a b, ∀ (H : ℝ), (∀ s ∈ Set.Icc a b, √(l2NormSq (F s)) ≤ H) → |∫ (s : ℝ) in anchor..t, hmRegularPairing s| ≤ √(b - a) * Gscale * H) (hfluxBound : ∀ t ∈ Set.Icc a b, |∫ (s : ℝ) in anchor..t, hmFluxPairing s| ≤ Q) (t : ℝ) : t ∈ Set.Icc a b → √(l2NormSq (F t)) ≤ 2 * √(b - a) * Gscale + √(2 * Q)

The transported norm estimate with its maximum chosen internally. The base point may be either end of the closed interval; this handles refresh cells that meet time zero by integrating backward from their positive right endpoint. hregBound is the time-integrated regular pairing estimate under an arbitrary cell envelope, and hfluxBound is the integrated signed flux pairing estimate.

theorem AVenhance.Infra.Section4.hm_continuous_slice_eLpNorm_le_of_l2NormSq_bound {f : Homogenization.Vec 2 → ℝ} {B : ℝ} (hf : Continuous f) (hB : 0 ≤ B) (hbound : √(l2NormSq f) ≤ B) : MeasureTheory.eLpNorm f 2 (MeasureTheory.volume.restrict unitCube) ≤ ENNReal.ofReal B

Convert the transported quadratic-energy bound to the eLpNorm field shape for a continuous periodic slice.

theorem AVenhance.Infra.Section4.frozen_hm_halfCell_endpoints_zero {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) (κ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (l : ℤ) : (I.Hm hΦ m κ T ((↑l + 1 / 2) * tauPP β I.Λ m) = fun (x : Homogenization.Vec 2) => 0) ∧ ∀ (x : Homogenization.Vec 2), Section5.hmEndpoint I hΦ m κ T (Jcut β) ((↑l + 1 / 2) * tauPP β I.Λ m) x - Section5.hmEndpoint I hΦ m κ T 0 ((↑l + 1 / 2) * tauPP β I.Λ m) x = 0

Both the potential and its material source vanish at each half-cell boundary.

theorem AVenhance.Infra.Section4.frozen_hm_halfCell_eLpNorm_bound {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) (κ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (l : ℤ) (X : ℝ → Ergodic.PeriodicVolumePreservingDiffeomorphism 2) {source : ℝ → Homogenization.Vec 2 → ℝ} (hFper : ∀ (t : ℝ), IsZ2Periodic (I.Hm hΦ m κ T t)) (hSourcePer : ∀ (t : ℝ), IsZ2Periodic (source t)) (hComp : ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => I.Hm hΦ m κ T 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 : ℝ) => I.Hm hΦ m κ T s ((X s).toFun x)) (source t ((X t).toFun x)) t) {b D B : ℝ} (hc : 0 < (↑l + 1 / 2) * tauPP β I.Λ m) (hcb : (↑l + 1 / 2) * tauPP β I.Λ m ≤ b) (hD : 0 ≤ D) (hB : 0 ≤ B) (hNormCont : ContinuousOn (fun (t : ℝ) => √(l2NormSq (I.Hm hΦ m κ T t))) (Set.Icc ((↑l + 1 / 2) * tauPP β I.Λ m) b)) (hSourceBound : ∀ t ∈ Set.Icc ((↑l + 1 / 2) * tauPP β I.Λ m) b, √(l2NormSq (source t)) ≤ D) (hScale : 2 * (b - (↑l + 1 / 2) * tauPP β I.Λ m) * D ≤ B) (hSliceCont : ∀ t ∈ Set.Icc ((↑l + 1 / 2) * tauPP β I.Λ m) b, Continuous (I.Hm hΦ m κ T t)) (t : ℝ) : t ∈ Set.Icc ((↑l + 1 / 2) * tauPP β I.Λ m) b → MeasureTheory.eLpNorm (I.Hm hΦ m κ T t) 2 (MeasureTheory.volume.restrict unitCube) ≤ ENNReal.ofReal B

The actual H_m vanishes at the left half-cell endpoint, so the transported FTC gives a cellwise L² bound without a norm-attainment or time-constant-norm premise. source is the scalar material derivative; its scale and amplitude stay abstract.