Space-time forcing estimates for the actual ordered coefficient flux.
theorem
AVenhance.Infra.Section4.IteratesTruncatedWeighted.iterate_integrable_list_sum
{α : Type u_1}
(P : List α)
(f : α → AmnrSpace → ℝ)
(hf : ∀ p ∈ P, MeasureTheory.IntegrableOn (f p) timeCube MeasureTheory.volume)
:
MeasureTheory.IntegrableOn (fun (z : AmnrSpace) => (List.map (fun (p : α) => f p z) P).sum) timeCube
MeasureTheory.volume
theorem
AVenhance.Infra.Section4.IteratesTruncatedWeighted.iterate_integral_list_sum
{α : Type u_1}
(P : List α)
(f : α → AmnrSpace → ℝ)
(hf : ∀ p ∈ P, MeasureTheory.IntegrableOn (f p) timeCube MeasureTheory.volume)
:
theorem
AVenhance.Infra.Section4.iterate_split_flux_spacetime_absolute_integral_bound
(P : List (List (Fin 2) × List (Fin 2)))
(A : ℝ → Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ)
(v : ℝ → Homogenization.Vec 2 → ℝ)
(a : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2)
(ρ D : List (Fin 2) × List (Fin 2) → ℝ)
(hρ : ∀ p ∈ P, 0 < ρ p)
(hAj :
∀ (t : ℝ) (x : Homogenization.Vec 2),
∀ p ∈ P, ∀ (i j : Fin 2), |iterateSpatialWord p.1 (fun (y : Homogenization.Vec 2) => A t y i j) x| ≤ D p)
(ha :
MeasureTheory.IntegrableOn (fun (z : AmnrSpace) => Homogenization.vecNormSq (a z.1 z.2)) timeCube
MeasureTheory.volume)
(hv :
∀ p ∈ P,
MeasureTheory.IntegrableOn
(fun (z : AmnrSpace) => Homogenization.vecNormSq (spaceGrad (iterateSpatialWord p.2 (v z.1)) z.2)) timeCube
MeasureTheory.volume)
(hp :
MeasureTheory.IntegrableOn
(fun (z : AmnrSpace) => Homogenization.vecDot (a z.1 z.2) (iterateSplitFlux P (A z.1) (v z.1) z.2)) timeCube
MeasureTheory.volume)
:
∫ (z : ℝ × Homogenization.Vec 2) in timeCube, |Homogenization.vecDot (a z.1 z.2) (iterateSplitFlux P (A z.1) (v z.1) z.2)| ≤ (List.map ρ P).sum * spaceTimeGradNormSq a + (List.map
(fun (p : List (Fin 2) × List (Fin 2)) =>
D p ^ 2 / ρ p * spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (iterateSpatialWord p.2 (v t)))
P).sum
Weighted all-order forcing control on the space-time cell. Integrability premises concern the actual fields; no quantitative forcing estimate or norm recurrence is assumed.
theorem
AVenhance.Infra.Section4.iterate_truncated_split_flux_pairing_bound
{s : ℝ}
(hs1 : s ≤ 1)
(P : List (List (Fin 2) × List (Fin 2)))
(A : ℝ → Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ)
(v : ℝ → Homogenization.Vec 2 → ℝ)
(a : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2)
(ρ D : List (Fin 2) × List (Fin 2) → ℝ)
(hρ : ∀ p ∈ P, 0 < ρ p)
(hAj :
∀ (t : ℝ) (x : Homogenization.Vec 2),
∀ p ∈ P, ∀ (i j : Fin 2), |iterateSpatialWord p.1 (fun (y : Homogenization.Vec 2) => A t y i j) x| ≤ D p)
(ha :
MeasureTheory.IntegrableOn (fun (z : AmnrSpace) => Homogenization.vecNormSq (a z.1 z.2)) timeCube
MeasureTheory.volume)
(hv :
∀ p ∈ P,
MeasureTheory.IntegrableOn
(fun (z : AmnrSpace) => Homogenization.vecNormSq (spaceGrad (iterateSpatialWord p.2 (v z.1)) z.2)) timeCube
MeasureTheory.volume)
(hp :
MeasureTheory.IntegrableOn
(fun (z : AmnrSpace) => Homogenization.vecDot (a z.1 z.2) (iterateSplitFlux P (A z.1) (v z.1) z.2)) timeCube
MeasureTheory.volume)
:
|∫ (z : AmnrSpace) in iterateTruncatedCell s, Homogenization.vecDot (a z.1 z.2) (iterateSplitFlux P (A z.1) (v z.1) z.2)| ≤ (List.map ρ P).sum * spaceTimeGradNormSq a + (List.map
(fun (p : List (Fin 2) × List (Fin 2)) =>
D p ^ 2 / ρ p * spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (iterateSpatialWord p.2 (v t)))
P).sum
Every terminal selected flux is bounded by the full nonnegative coefficient-gradient allocation, retaining exact ordered multiplicities.