Pairing inputs for a positive-time Hm cell. Spacetime L² bounds are converted to the time-slice data used by the regular and flux Cauchy estimates. The time-continuity of the scalar pairings is kept as an explicit interface; the actual-flow continuity lemmas can discharge it.

def AVenhance.Infra.Section4.HmPerTimePairingInputs.hmPairingClosedCube : Set (Homogenization.Vec 2)

Closed spatial unit cell used for compactness and periodic integration.

Equations

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

theorem AVenhance.Infra.Section4.HmPerTimePairingInputs.hmPairingClosedCube_compact : IsCompact hmPairingClosedCube

theorem AVenhance.Infra.Section4.HmPerTimePairingInputs.hmPairingUnitCube_ae_eq_closedCube : unitCube =ᵐ[MeasureTheory.volume] hmPairingClosedCube

def AVenhance.Infra.Section4.HmPerTimePairingInputs.hmPairingTimeClamp (a b t : ℝ) : ℝ

Clamp time between two endpoints for the per-time Hm pairing.

Equations

• AVenhance.Infra.Section4.HmPerTimePairingInputs.hmPairingTimeClamp a b t = max a (min t b)

theorem AVenhance.Infra.Section4.HmPerTimePairingInputs.hmPairingTimeClamp_continuous (a b : ℝ) : Continuous (hmPairingTimeClamp a b)

theorem AVenhance.Infra.Section4.HmPerTimePairingInputs.hmPairingTimeClamp_mem {a b t : ℝ} (hab : a ≤ b) : hmPairingTimeClamp a b t ∈ Set.Icc a b

theorem AVenhance.Infra.Section4.HmPerTimePairingInputs.hmPairingTimeClamp_eq {a b t : ℝ} (ht : t ∈ Set.Icc a b) : hmPairingTimeClamp a b t = t

theorem AVenhance.Infra.Section4.HmPerTimePairingInputs.hm_spaceGrad_continuous_of_contDiff {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ 1 f) : Continuous (spaceGrad f)

theorem AVenhance.Infra.Section4.hm_pairing_continuity_of_joint_fields {F G : ℝ → Homogenization.Vec 2 → ℝ} {V : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {a b : ℝ} (hab : a ≤ b) (hFJoint : ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => F p.1 p.2) (Set.Icc a b ×ˢ Set.univ)) (hGJoint : ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => G p.1 p.2) (Set.Icc a b ×ˢ Set.univ)) (hDivJoint : ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => vecDiv (V p.1) p.2) (Set.Icc a b ×ˢ Set.univ)) (hFper : ∀ t ∈ Set.Icc a b, IsZ2Periodic (F t)) (hVper : ∀ t ∈ Set.Icc a b, ∀ (i : Fin 2), IsZ2Periodic fun (x : Homogenization.Vec 2) => V t x i) (hF : ∀ t ∈ Set.Icc a b, ContDiff ℝ 1 (F t)) (hV : ∀ t ∈ Set.Icc a b, ContDiff ℝ 1 (V t)) : ContinuousOn hmRegularPairing (Set.Icc a b) ∧ ContinuousOn hmFluxPairing (Set.Icc a b)

Joint continuity of the scalar fields on a positive time cell implies continuity of both time pairings. For the flux term, periodic integration by parts rewrites the gradient--vector pairing as the integral of F * div V; this uses only joint continuity of the divergence field.

theorem AVenhance.Infra.Section4.hm_per_time_pairing_inputs_of_spacetime_eLpNorm {F G : ℝ → Homogenization.Vec 2 → ℝ} {V : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {a b anchor QG Qgrad QV : ℝ} (ha : 0 < a) (hb : b ≤ 1) (hanchor : anchor ∈ Set.Icc a b) (hFcont : ∀ (s : ℝ), 0 < s → Continuous (F s)) (hGcont : ∀ (s : ℝ), 0 < s → Continuous (G s)) (hGradCont : ∀ (s : ℝ), 0 < s → Continuous (spaceGrad (F s))) (hVcont : ∀ (s : ℝ), 0 < s → Continuous (V s)) (hGmeas : MeasureTheory.AEStronglyMeasurable (fun (z : ℝ × Homogenization.Vec 2) => G z.1 z.2) (MeasureTheory.volume.restrict timeCube)) (hQG : 0 ≤ QG) (hGbound : MeasureTheory.eLpNorm (fun (z : ℝ × Homogenization.Vec 2) => G z.1 z.2) 2 (MeasureTheory.volume.restrict timeCube) ≤ ENNReal.ofReal QG) (hGradMeas : MeasureTheory.AEStronglyMeasurable (fun (z : ℝ × Homogenization.Vec 2) => spaceGrad (F z.1) z.2) (MeasureTheory.volume.restrict timeCube)) (hGradMagMeas : MeasureTheory.AEStronglyMeasurable (fun (z : ℝ × Homogenization.Vec 2) => √(Homogenization.vecNormSq (spaceGrad (F z.1) z.2))) (MeasureTheory.volume.restrict timeCube)) (hQgrad : 0 ≤ Qgrad) (hGradBound : MeasureTheory.eLpNorm (fun (z : ℝ × Homogenization.Vec 2) => spaceGrad (F z.1) z.2) 2 (MeasureTheory.volume.restrict timeCube) ≤ ENNReal.ofReal Qgrad) (hVmeas : MeasureTheory.AEStronglyMeasurable (fun (z : ℝ × Homogenization.Vec 2) => V z.1 z.2) (MeasureTheory.volume.restrict timeCube)) (hVmagMeas : MeasureTheory.AEStronglyMeasurable (fun (z : ℝ × Homogenization.Vec 2) => √(Homogenization.vecNormSq (V z.1 z.2))) (MeasureTheory.volume.restrict timeCube)) (hQV : 0 ≤ QV) (hVbound : MeasureTheory.eLpNorm (fun (z : ℝ × Homogenization.Vec 2) => V z.1 z.2) 2 (MeasureTheory.volume.restrict timeCube) ≤ ENNReal.ofReal QV) (hRegPairCont : ContinuousOn hmRegularPairing (Set.Icc a b)) (hFluxPairCont : ContinuousOn hmFluxPairing (Set.Icc a b)) : (∀ s ∈ Set.Icc a b, IntervalIntegrable hmRegularPairing MeasureTheory.volume anchor s) ∧ (∀ s ∈ Set.Icc a b, IntervalIntegrable hmFluxPairing MeasureTheory.volume anchor s) ∧ (∀ (H' : ℝ), (∀ s ∈ Set.Icc a b, √(l2NormSq (F s)) ≤ H') → ∀ s ∈ Set.Icc a b, |∫ (r : ℝ) in anchor..s, hmRegularPairing r| ≤ √(max anchor s - min anchor s) * QG * H') ∧ ∀ s ∈ Set.Icc a b, |∫ (r : ℝ) in anchor..s, hmFluxPairing r| ≤ √2 * Qgrad * (√2 * QV)

On a positive cell, spacetime L² bounds for the regular source, the Hm gradient, and the divergence remainder give the local pairing inputs used by the per-time half-cell assembler. The two vector bounds carry the explicit √2 conversion from the Pi norm on Vec 2 to Euclidean energy.

theorem AVenhance.Infra.Section4.hm_per_time_pairing_data_of_spacetime_eLpNorm {F G : ℝ → Homogenization.Vec 2 → ℝ} {V : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {c : ℝ → ℝ} {QG Qgrad QV : ℝ} (hEndpoint : ∀ t ∈ Set.Ioc 0 1, 0 < c t ∧ c t ≤ 1) (hFcont : ∀ (s : ℝ), 0 < s → Continuous (F s)) (hGcont : ∀ (s : ℝ), 0 < s → Continuous (G s)) (hGradCont : ∀ (s : ℝ), 0 < s → Continuous (spaceGrad (F s))) (hVcont : ∀ (s : ℝ), 0 < s → Continuous (V s)) (hGmeas : MeasureTheory.AEStronglyMeasurable (fun (z : ℝ × Homogenization.Vec 2) => G z.1 z.2) (MeasureTheory.volume.restrict timeCube)) (hQG : 0 ≤ QG) (hGbound : MeasureTheory.eLpNorm (fun (z : ℝ × Homogenization.Vec 2) => G z.1 z.2) 2 (MeasureTheory.volume.restrict timeCube) ≤ ENNReal.ofReal QG) (hGradMeas : MeasureTheory.AEStronglyMeasurable (fun (z : ℝ × Homogenization.Vec 2) => spaceGrad (F z.1) z.2) (MeasureTheory.volume.restrict timeCube)) (hGradMagMeas : MeasureTheory.AEStronglyMeasurable (fun (z : ℝ × Homogenization.Vec 2) => √(Homogenization.vecNormSq (spaceGrad (F z.1) z.2))) (MeasureTheory.volume.restrict timeCube)) (hQgrad : 0 ≤ Qgrad) (hGradBound : MeasureTheory.eLpNorm (fun (z : ℝ × Homogenization.Vec 2) => spaceGrad (F z.1) z.2) 2 (MeasureTheory.volume.restrict timeCube) ≤ ENNReal.ofReal Qgrad) (hVmeas : MeasureTheory.AEStronglyMeasurable (fun (z : ℝ × Homogenization.Vec 2) => V z.1 z.2) (MeasureTheory.volume.restrict timeCube)) (hVmagMeas : MeasureTheory.AEStronglyMeasurable (fun (z : ℝ × Homogenization.Vec 2) => √(Homogenization.vecNormSq (V z.1 z.2))) (MeasureTheory.volume.restrict timeCube)) (hQV : 0 ≤ QV) (hVbound : MeasureTheory.eLpNorm (fun (z : ℝ × Homogenization.Vec 2) => V z.1 z.2) 2 (MeasureTheory.volume.restrict timeCube) ≤ ENNReal.ofReal QV) (hRegPairCont : ∀ t ∈ Set.Ioc 0 1, ContinuousOn hmRegularPairing (Set.Icc (min (c t) t) (max (c t) t))) (hFluxPairCont : ∀ t ∈ Set.Ioc 0 1, ContinuousOn hmFluxPairing (Set.Icc (min (c t) t) (max (c t) t))) : (∀ t ∈ Set.Ioc 0 1, ∀ s ∈ Set.Icc (min (c t) t) (max (c t) t), IntervalIntegrable hmRegularPairing MeasureTheory.volume (c t) s) ∧ (∀ t ∈ Set.Ioc 0 1, ∀ s ∈ Set.Icc (min (c t) t) (max (c t) t), IntervalIntegrable hmFluxPairing MeasureTheory.volume (c t) s) ∧ (∀ t ∈ Set.Ioc 0 1, ∀ (H : ℝ), (∀ s ∈ Set.Icc (min (c t) t) (max (c t) t), √(l2NormSq (F s)) ≤ H) → ∀ s ∈ Set.Icc (min (c t) t) (max (c t) t), |∫ (r : ℝ) in c t..s, hmRegularPairing r| ≤ √(max (c t) t - min (c t) t) * QG * H) ∧ ∀ t ∈ Set.Ioc 0 1, ∀ s ∈ Set.Icc (min (c t) t) (max (c t) t), |∫ (r : ℝ) in c t..s, hmFluxPairing r| ≤ √2 * Qgrad * (√2 * QV)

Uniform-in-time form of the local pairing bridge, with a varying positive base point c t. This supplies exactly the four pairing fields consumed by frozen_hm_positive_time_bounds_of_pairings_per_time.

theorem AVenhance.Infra.Section4.hm_per_time_pairing_data_of_joint_fields_and_spacetime_eLpNorm {F G : ℝ → Homogenization.Vec 2 → ℝ} {V : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {c : ℝ → ℝ} {QG Qgrad QV : ℝ} (hEndpoint : ∀ t ∈ Set.Ioc 0 1, 0 < c t ∧ c t ≤ 1) (hFper : ∀ (t : ℝ), 0 < t → IsZ2Periodic (F 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)) (hV : ∀ (t : ℝ), 0 < t → ContDiff ℝ 1 (V t)) (hFJoint : ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => F p.1 p.2) (Set.Ioi 0 ×ˢ Set.univ)) (hGJoint : ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => G p.1 p.2) (Set.Ioi 0 ×ˢ Set.univ)) (hDivJoint : ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => vecDiv (V p.1) p.2) (Set.Ioi 0 ×ˢ Set.univ)) (hGmeas : MeasureTheory.AEStronglyMeasurable (fun (z : ℝ × Homogenization.Vec 2) => G z.1 z.2) (MeasureTheory.volume.restrict timeCube)) (hQG : 0 ≤ QG) (hGbound : MeasureTheory.eLpNorm (fun (z : ℝ × Homogenization.Vec 2) => G z.1 z.2) 2 (MeasureTheory.volume.restrict timeCube) ≤ ENNReal.ofReal QG) (hGradMeas : MeasureTheory.AEStronglyMeasurable (fun (z : ℝ × Homogenization.Vec 2) => spaceGrad (F z.1) z.2) (MeasureTheory.volume.restrict timeCube)) (hGradMagMeas : MeasureTheory.AEStronglyMeasurable (fun (z : ℝ × Homogenization.Vec 2) => √(Homogenization.vecNormSq (spaceGrad (F z.1) z.2))) (MeasureTheory.volume.restrict timeCube)) (hQgrad : 0 ≤ Qgrad) (hGradBound : MeasureTheory.eLpNorm (fun (z : ℝ × Homogenization.Vec 2) => spaceGrad (F z.1) z.2) 2 (MeasureTheory.volume.restrict timeCube) ≤ ENNReal.ofReal Qgrad) (hVmeas : MeasureTheory.AEStronglyMeasurable (fun (z : ℝ × Homogenization.Vec 2) => V z.1 z.2) (MeasureTheory.volume.restrict timeCube)) (hVmagMeas : MeasureTheory.AEStronglyMeasurable (fun (z : ℝ × Homogenization.Vec 2) => √(Homogenization.vecNormSq (V z.1 z.2))) (MeasureTheory.volume.restrict timeCube)) (hQV : 0 ≤ QV) (hVbound : MeasureTheory.eLpNorm (fun (z : ℝ × Homogenization.Vec 2) => V z.1 z.2) 2 (MeasureTheory.volume.restrict timeCube) ≤ ENNReal.ofReal QV) : (∀ t ∈ Set.Ioc 0 1, ∀ s ∈ Set.Icc (min (c t) t) (max (c t) t), IntervalIntegrable hmRegularPairing MeasureTheory.volume (c t) s) ∧ (∀ t ∈ Set.Ioc 0 1, ∀ s ∈ Set.Icc (min (c t) t) (max (c t) t), IntervalIntegrable hmFluxPairing MeasureTheory.volume (c t) s) ∧ (∀ t ∈ Set.Ioc 0 1, ∀ (H : ℝ), (∀ s ∈ Set.Icc (min (c t) t) (max (c t) t), √(l2NormSq (F s)) ≤ H) → ∀ s ∈ Set.Icc (min (c t) t) (max (c t) t), |∫ (r : ℝ) in c t..s, hmRegularPairing r| ≤ √(max (c t) t - min (c t) t) * QG * H) ∧ ∀ t ∈ Set.Ioc 0 1, ∀ s ∈ Set.Icc (min (c t) t) (max (c t) t), |∫ (r : ℝ) in c t..s, hmFluxPairing r| ≤ √2 * Qgrad * (√2 * QV)

Obtain the time-pairing continuity from positive-time joint continuity of F, the regular source, and div V. This is the interface to the actual-flow regularity producer: its periodic C¹ fields and its joint source formulas give these hypotheses cell by cell.