Positive-time spacetime measurability and finite-L² adapters for the
three fields used by the H_m per-time pairing interface. Quantitative rate
constants remain producer inputs: the Piola-source rate is supplied
directly, while the gradient and d_m rates are read from
HmGradientContract and SourceErrorDContract. The separate adapter
below bounds only the legacy (flux - Kmat) : ∇Gbar contraction.
theorem
AVenhance.Infra.Section4.HmMeasurability.hm_meas_d_joint
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
{m : ℕ}
(hm : 1 ≤ m)
{κ κprev : ℝ}
(hκ : 0 < κ)
{θ₀ : Homogenization.Vec 2 → ℝ}
{θprev : ℝ → Homogenization.Vec 2 → ℝ}
{Titer : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hθprev : IsClassicalSol (streamVel (Φ (m - 1))) κprev (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θprev)
(hT : I.IsTIterates hΦ m κ κprev θ₀ θprev Titer)
:
ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => Section5.sourceErrorD I hΦ m κ (Titer (Nstar β)) p.1 p.2)
(Set.Ioi 0 ×ˢ Set.univ)
theorem
AVenhance.Infra.Section4.hm_actual_pairing_field_measurability
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
{m : ℕ}
(hm : 1 ≤ m)
{κ κprev : ℝ}
(hκ : 0 < κ)
{θ₀ : Homogenization.Vec 2 → ℝ}
{θprev : ℝ → Homogenization.Vec 2 → ℝ}
{Titer : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hθprev : IsClassicalSol (streamVel (Φ (m - 1))) κprev (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θprev)
(hT : I.IsTIterates hΦ m κ κprev θ₀ θprev Titer)
:
MeasureTheory.AEStronglyMeasurable
(fun (z : ℝ × Homogenization.Vec 2) => hmFrozenPiolaSource I hΦ m κ (Titer (Nstar β)) z.1 z.2)
(MeasureTheory.volume.restrict timeCube) ∧ MeasureTheory.AEStronglyMeasurable
(fun (z : ℝ × Homogenization.Vec 2) => spaceGrad (I.Hm hΦ m κ (Titer (Nstar β)) z.1) z.2)
(MeasureTheory.volume.restrict timeCube) ∧ MeasureTheory.AEStronglyMeasurable
(fun (z : ℝ × Homogenization.Vec 2) =>
√(Homogenization.vecNormSq (spaceGrad (I.Hm hΦ m κ (Titer (Nstar β)) z.1) z.2)))
(MeasureTheory.volume.restrict timeCube) ∧ MeasureTheory.AEStronglyMeasurable
(fun (z : ℝ × Homogenization.Vec 2) => Section5.sourceErrorD I hΦ m κ (Titer (Nstar β)) z.1 z.2)
(MeasureTheory.volume.restrict timeCube) ∧ MeasureTheory.AEStronglyMeasurable
(fun (z : ℝ × Homogenization.Vec 2) =>
√(Homogenization.vecNormSq (Section5.sourceErrorD I hΦ m κ (Titer (Nstar β)) z.1 z.2)))
(MeasureTheory.volume.restrict timeCube)
The five AEStronglyMeasurable fields consumed by
hm_per_time_pairing_data_of_joint_fields_and_spacetime_eLpNorm, deduced from
the actual joint-continuity construction.
theorem
AVenhance.Infra.Section4.hm_gradient_spacetime_eLpNorm_bound_of_contract
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
{m : ℕ}
(hm : 1 ≤ m)
{κ κprev : ℝ}
(hκ : 0 < κ)
(hκprev : 0 < κprev)
{θ₀ : Homogenization.Vec 2 → ℝ}
{θprev : ℝ → Homogenization.Vec 2 → ℝ}
{Titer : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
{CH B : ℝ}
(hθprev : IsClassicalSol (streamVel (Φ (m - 1))) κprev (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θprev)
(hT : I.IsTIterates hΦ m κ κprev θ₀ θprev Titer)
(hCH : 0 ≤ CH)
(hB : 0 ≤ B)
(hContract : Section5.Integration.HmGradientContract I hΦ m κ κprev Titer CH B)
:
HmGradientContract gives the spacetime vector L² bound consumed by
the pairing assembler. The closed-time extension supplies the integrability
needed to interpret its real-valued energy as an actual square integral.
theorem
AVenhance.Infra.Section4.HmMeasurability.hm_vector_spacetime_eLpNorm_bound_of_slice_energy
{V : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2}
{Q : ℝ}
(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))
(hVslice : ∀ t ∈ Set.Ioo 0 1, Continuous (V t))
(_hQ : 0 ≤ Q)
(hEnergy : (∫⁻ (t : ℝ) in Set.Ioo 0 1, ENNReal.ofReal √(gradNormSq (V t)) ^ 2) ^ (1 / 2) ≤ ENNReal.ofReal Q)
:
MeasureTheory.eLpNorm (fun (z : ℝ × Homogenization.Vec 2) => V z.1 z.2) 2 (MeasureTheory.volume.restrict timeCube) ≤ ENNReal.ofReal Q
theorem
AVenhance.Infra.Section4.hm_sourceErrorD_spacetime_eLpNorm_bound_of_contract
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
{m : ℕ}
(hm : 1 ≤ m)
{κ κprev : ℝ}
(hκ : 0 < κ)
{θ₀ : Homogenization.Vec 2 → ℝ}
{θprev : ℝ → Homogenization.Vec 2 → ℝ}
{Titer : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
{Cd B : ℝ}
(hθprev : IsClassicalSol (streamVel (Φ (m - 1))) κprev (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θprev)
(hT : I.IsTIterates hΦ m κ κprev θ₀ θprev Titer)
(hCd : 0 ≤ Cd)
(hB : 0 ≤ B)
(hContract : Section5.Integration.SourceErrorDContract I hΦ m κ Titer Cd B)
:
MeasureTheory.eLpNorm (fun (z : ℝ × Homogenization.Vec 2) => Section5.sourceErrorD I hΦ m κ (Titer (Nstar β)) z.1 z.2) 2
(MeasureTheory.volume.restrict timeCube) ≤ ENNReal.ofReal (Cd * epsilon β I.Λ (m - 1) ^ (2 * delta β) * √κ * B)
The SourceErrorDContract time-slice Euclidean rate supplies the matching
spacetime eLpNorm bound for d_m, with the same source-rate constant.