Positive-time H_m assembly when the half-cell base point may vary with time.
The regular pairing retains its raw source coefficient; the scalar energy
closure uses the square-root-length gain supplied by HmHalfCellGain.
noncomputable def
AVenhance.Infra.Section4.hmHalfCellEndpointAt
{β : ℝ}
(I : Ingredients β)
(m : ℕ)
(l : ℝ → ℤ)
(t : ℝ)
:
The refresh endpoint selected at time t by an index function l.
Equations
- AVenhance.Infra.Section4.hmHalfCellEndpointAt I m l t = (↑(l t) + 1 / 2) * AVenhance.tauPP β I.Λ m
Instances For
theorem
AVenhance.Infra.Section4.hm_positive_time_halfCell_index_of_gain
{β : ℝ}
(I : Ingredients β)
{m : ℕ}
{Gsource Ghalf : ℝ}
(hGain :
∀ t ∈ Set.Ioc 0 1,
∃ (j : ℤ),
have c := (↑j + 1 / 2) * tauPP β I.Λ m;
0 < c ∧ c ≤ 1 ∧ max c t - min c t ≤ tauPP β I.Λ m ∧ √(max c t - min c t) * Gsource ≤ Ghalf)
:
∃ (l : ℝ → ℤ),
(∀ t ∈ Set.Ioc 0 1,
0 < hmHalfCellEndpointAt I m l t ∧ hmHalfCellEndpointAt I m l t ≤ 1 ∧ max (hmHalfCellEndpointAt I m l t) t - min (hmHalfCellEndpointAt I m l t) t ≤ tauPP β I.Λ m) ∧ ∀ t ∈ Set.Ioc 0 1, √(max (hmHalfCellEndpointAt I m l t) t - min (hmHalfCellEndpointAt I m l t) t) * Gsource ≤ Ghalf
Turn the existential endpoint and coefficient gain from
hm_positive_time_halfCell_source_gain_from_A5 into the function-valued
interface used by the per-time assembler.
theorem
AVenhance.Infra.Section4.frozen_hm_positive_time_bounds_of_pairings_per_time
{β : ℝ}
(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) =>
hmFrozenRegularSource 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 (hmFrozenRegularSource 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) =>
hmFrozenRegularSource 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) =>
hmFrozenRegularSource I hΦ m κ T t y + vecDiv (Section5.sourceErrorD I hΦ m κ T t) y)
((X t).toFun x))
t)
{Gsource Ghalf Q C₀ E δ Θ C₁ Khalf : ℝ}
(l : ℝ → ℤ)
(hEndpoint :
∀ t ∈ Set.Ioc 0 1,
0 < hmHalfCellEndpointAt I m l t ∧ hmHalfCellEndpointAt I m l t ≤ 1 ∧ max (hmHalfCellEndpointAt I m l t) t - min (hmHalfCellEndpointAt I m l t) t ≤ tauPP β I.Λ m)
(hHalfGain :
∀ t ∈ Set.Ioc 0 1, √(max (hmHalfCellEndpointAt I m l t) t - min (hmHalfCellEndpointAt I m l t) t) * Gsource ≤ Ghalf)
(hNormCont :
∀ t ∈ Set.Ioc 0 1,
ContinuousOn (fun (s : ℝ) => √(l2NormSq (I.Hm hΦ m κ T s)))
(Set.Icc (min (hmHalfCellEndpointAt I m l t) t) (max (hmHalfCellEndpointAt I m l t) t)))
(hregInt :
∀ t ∈ Set.Ioc 0 1,
∀ s ∈ Set.Icc (min (hmHalfCellEndpointAt I m l t) t) (max (hmHalfCellEndpointAt I m l t) t),
IntervalIntegrable hmRegularPairing MeasureTheory.volume (hmHalfCellEndpointAt I m l t) s)
(hfluxInt :
∀ t ∈ Set.Ioc 0 1,
∀ s ∈ Set.Icc (min (hmHalfCellEndpointAt I m l t) t) (max (hmHalfCellEndpointAt I m l t) t),
IntervalIntegrable hmFluxPairing MeasureTheory.volume (hmHalfCellEndpointAt I m l t) s)
(hregBound :
∀ t ∈ Set.Ioc 0 1,
∀ (H : ℝ),
(∀ s ∈ Set.Icc (min (hmHalfCellEndpointAt I m l t) t) (max (hmHalfCellEndpointAt I m l t) t),
√(l2NormSq (I.Hm hΦ m κ T s)) ≤ H) →
∀ s ∈ Set.Icc (min (hmHalfCellEndpointAt I m l t) t) (max (hmHalfCellEndpointAt I m l t) t),
|∫ (r : ℝ) in hmHalfCellEndpointAt I m l t..s, hmRegularPairing r| ≤ √(max (hmHalfCellEndpointAt I m l t) t - min (hmHalfCellEndpointAt I m l t) t) * Gsource * H)
(hfluxBound :
∀ t ∈ Set.Ioc 0 1,
∀ s ∈ Set.Icc (min (hmHalfCellEndpointAt I m l t) t) (max (hmHalfCellEndpointAt I m l t) t),
|∫ (r : ℝ) in hmHalfCellEndpointAt I m l t..s, hmFluxPairing r| ≤ Q)
(hGsourceNonneg : 0 ≤ Gsource)
(hQnonneg : 0 ≤ Q)
(hScale : 2 * Ghalf + √(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 * Θ)
Assemble the positive-time H_m bounds with a time-dependent refresh
index. The regular pairing hypothesis uses the raw coefficient Gsource:
its Cauchy bound contains sqrt(interval length) * Gsource. The endpoint
gain hypothesis bounds that product by Ghalf, which is the coefficient
used in the scalar energy closure. This is the interface consumed by the
per-time half-cell estimate.