Per-scale assembly for the source-form §2 flow bounds.
theorem
AVenhance.Infra.Construction.section2_spatial_flow_data_from_previous
{β : ℝ}
{I : Ingredients β}
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
{hseq : IsStreamSeq I Φ}
{R M : ℕ → ℝ}
(hscales : Section2Scales I R M)
(happB2 : AppB2InverseFlowData I Φ hseq R M)
(m : ℕ)
(hm : 1 ≤ m)
(hprev : Section2StreamInductionHypothesis R M (m - 1))
:
Section2SpatialFlowData I Φ hseq m
The spatial inputs to the material-Jacobian estimate follow directly from the preceding Section 2 induction hypothesis.
theorem
AVenhance.Infra.Construction.section2_flow_bounds_at_scale_from_previous
{β : ℝ}
{I : Ingredients β}
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
{hseq : IsStreamSeq I Φ}
{R M : ℕ → ℝ}
{Cmat : ℝ}
(hscales : Section2Scales I R M)
(happB2 : AppB2InverseFlowData I Φ hseq R M)
(m : ℕ)
(hm : 1 ≤ m)
(hprev : Section2StreamInductionHypothesis R M (m - 1))
(hmaterial :
∀ (s t : ℝ),
|t| ≤ 2 ^ (-25) * (a β I.Λ m)⁻¹ →
∀ (n ell : ℕ),
n + ell ≤ Nstar β →
∀ (i j : Fin 2) (x : Homogenization.Vec 2) (J : Fin n → Fin 2),
‖(iteratedFDeriv ℝ n
(fun (y : Homogenization.Vec 2) =>
constructionMaterialIterate (fun (r : ℝ) (z : Homogenization.Vec 2) => streamVel (Φ m) (s + r) z)
ell
(fun (r : ℝ) (z : Homogenization.Vec 2) =>
(constructionComposedFlowJacobian hseq m s r z) (Homogenization.basisVec j) i)
t y)
x)
fun (k : Fin n) => Homogenization.basisVec (J k)‖ ≤ Cmat * (epsilon β I.Λ m)⁻¹ ^ n * (epsilon β I.Λ m ^ (β - 2)) ^ ell)
:
Section2FlowBoundsAtScale I Φ hseq Cmat m
Assemble the eight fields of Section2FlowBoundsAtScale
from the preceding scale. The final parameter is the disjoint
material_jacobian field.