Positive-time H_m assembly from a positive half-cell base point. The
extension-dependent value H_m(0) is never used.
theorem
AVenhance.Infra.Section4.hm_pairing_scale_of_l2_source_rates
{E δ ρ Θ κ Creg Cgrad Cdm G Grad D : ℝ}
(hE : 0 < E)
(hE1 : E ≤ 1)
(hδ : 0 < δ)
(hρ : 0 ≤ ρ)
(hΘ : 0 ≤ Θ)
(hκ : 0 < κ)
(hCgrad : 0 ≤ Cgrad)
(hCdm : 0 ≤ Cdm)
(hD : 0 ≤ D)
(hGreg : G ≤ Creg * E ^ δ * Θ)
(hGradRate : Grad ≤ Cgrad * E ^ (4 * δ) * (√κ)⁻¹ * Θ)
(hDRate : D ≤ Cdm * √κ * Θ * E ^ ρ)
:
Scalar closure for the positive-time pairing estimate. The regular
source has its direct E^δ Θ rate, while the flux pairing is the product of
the E^(4δ) Θ / √κ gradient rate and an E^ρ √κ Θ vector-source rate. The
κ factors cancel before taking the square root, leaving the same abstract
amplitude Θ; in particular this applies to the gradient normalization.
theorem
AVenhance.Infra.Section4.frozen_hm_positive_time_bounds_of_pairings
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
{m : ℕ}
(hm : 1 ≤ m)
(κ : ℝ)
(T : ℝ → Homogenization.Vec 2 → ℝ)
(X : ℝ → Ergodic.PeriodicVolumePreservingDiffeomorphism 2)
(hFper : ∀ (t : ℝ), 0 < t → IsZ2Periodic (I.Hm hΦ m κ T t))
(hSourcePer :
∀ (t : ℝ),
0 < t →
IsZ2Periodic fun (x : Homogenization.Vec 2) =>
hmFrozenPiolaSource I hΦ m κ T t x + vecDiv (Section5.sourceErrorD I hΦ m κ T t) x)
(hVper :
∀ (t : ℝ),
0 < t → ∀ (i : Fin 2), IsZ2Periodic fun (x : Homogenization.Vec 2) => Section5.sourceErrorD I hΦ m κ T t x i)
(hF : ∀ (t : ℝ), 0 < t → ContDiff ℝ 1 (I.Hm hΦ m κ T t))
(hG : ∀ (t : ℝ), 0 < t → Continuous (hmFrozenPiolaSource I hΦ m κ T t))
(hV : ∀ (t : ℝ), 0 < t → ContDiff ℝ 1 (Section5.sourceErrorD I hΦ m κ T 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) =>
(fun (x : Homogenization.Vec 2) =>
hmFrozenPiolaSource I hΦ m κ T p.1 x + vecDiv (Section5.sourceErrorD I hΦ m κ T p.1) x)
((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))
((fun (y : Homogenization.Vec 2) =>
hmFrozenPiolaSource I hΦ m κ T t y + vecDiv (Section5.sourceErrorD I hΦ m κ T t) y)
((X t).toFun x))
t)
{G Q C₀ E δ Θ C₁ Khalf : ℝ}
(l : ℤ)
(hc : 0 < (↑l + 1 / 2) * tauPP β I.Λ m)
(hc1 : (↑l + 1 / 2) * tauPP β I.Λ m ≤ 1)
(hNormCont :
∀ t ∈ Set.Ioc 0 1,
ContinuousOn (fun (s : ℝ) => √(l2NormSq (I.Hm hΦ m κ T s)))
(Set.Icc (min ((↑l + 1 / 2) * tauPP β I.Λ m) t) (max ((↑l + 1 / 2) * tauPP β I.Λ m) t)))
(hregInt :
∀ t ∈ Set.Ioc 0 1,
∀ s ∈ Set.Icc (min ((↑l + 1 / 2) * tauPP β I.Λ m) t) (max ((↑l + 1 / 2) * tauPP β I.Λ m) t),
IntervalIntegrable hmRegularPairing MeasureTheory.volume ((↑l + 1 / 2) * tauPP β I.Λ m) s)
(hfluxInt :
∀ t ∈ Set.Ioc 0 1,
∀ s ∈ Set.Icc (min ((↑l + 1 / 2) * tauPP β I.Λ m) t) (max ((↑l + 1 / 2) * tauPP β I.Λ m) t),
IntervalIntegrable hmFluxPairing MeasureTheory.volume ((↑l + 1 / 2) * tauPP β I.Λ m) s)
(hregBound :
∀ t ∈ Set.Ioc 0 1,
∀ (H : ℝ),
(∀ s ∈ Set.Icc (min ((↑l + 1 / 2) * tauPP β I.Λ m) t) (max ((↑l + 1 / 2) * tauPP β I.Λ m) t),
√(l2NormSq (I.Hm hΦ m κ T s)) ≤ H) →
∀ s ∈ Set.Icc (min ((↑l + 1 / 2) * tauPP β I.Λ m) t) (max ((↑l + 1 / 2) * tauPP β I.Λ m) t),
|∫ (r : ℝ) in (↑l + 1 / 2) * tauPP β I.Λ m..s, hmRegularPairing r| ≤ √(max ((↑l + 1 / 2) * tauPP β I.Λ m) t - min ((↑l + 1 / 2) * tauPP β I.Λ m) t) * G * H)
(hfluxBound :
∀ t ∈ Set.Ioc 0 1,
∀ s ∈ Set.Icc (min ((↑l + 1 / 2) * tauPP β I.Λ m) t) (max ((↑l + 1 / 2) * tauPP β I.Λ m) t),
|∫ (r : ℝ) in (↑l + 1 / 2) * tauPP β I.Λ m..s, hmFluxPairing r| ≤ Q)
(hGnonneg : 0 ≤ G)
(hQnonneg : 0 ≤ Q)
(hScale : 2 * G + √(2 * Q) ≤ C₀ * E ^ δ * Θ)
(hD :
∀ r ∈ Finset.range (Jcut β),
∀ (t : ℝ) (x : Homogenization.Vec 2), DifferentiableAt ℝ (fun (y : Homogenization.Vec 2) => I.Hmr hΦ m κ T r t y) x)
(hGradHmr :
∀ r ∈ Finset.range (Jcut β),
MeasureTheory.eLpNorm
(fun (z : ℝ × Homogenization.Vec 2) => spaceGrad (fun (x : Homogenization.Vec 2) => I.Hmr hΦ m κ T r z.1 x) z.2)
2 (MeasureTheory.volume.restrict timeCube) ≤ ENNReal.ofReal (C₁ * E ^ (4 * δ) * Khalf * Θ))
(hE : 0 ≤ E)
(hC₁ : 0 ≤ C₁)
(hΘ : 0 ≤ Θ)
(hKhalf : 0 ≤ Khalf)
:
(∀ t ∈ Set.Ioc 0 1, √(l2NormSq (I.Hm hΦ m κ T t)) ≤ C₀ * E ^ δ * Θ) ∧ MeasureTheory.eLpNorm
(fun (z : ℝ × Homogenization.Vec 2) => spaceGrad (fun (x : Homogenization.Vec 2) => I.Hm hΦ m κ T z.1 x) z.2) 2
(MeasureTheory.volume.restrict timeCube) ≤ ENNReal.ofReal (↑(Jcut β) * C₁ * E ^ (4 * δ) * Khalf * Θ)
Pairing FTC on the positive half-cell adjacent to zero and on the rest of
(0,1]. The base point is the positive half-cell endpoint where H_m
vanishes. Signed flux contributions stay in the gradient pairing.