Material induction simultaneously across the actual temperature family.
theorem
AVenhance.Infra.Section4.amnr_tIterates_material_gradient_induction
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
{m : ℕ}
(hm : 1 ≤ m)
{κm κprev : ℝ}
(hκm : 0 < κm)
(hκprev : 0 < κprev)
{θ₀ : Homogenization.Vec 2 → ℝ}
{θprev : ℝ → Homogenization.Vec 2 → ℝ}
{T : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hθprev : IsClassicalSol (streamVel (Φ (m - 1))) κprev (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θprev)
(hT : I.IsTIterates hΦ m κm κprev θ₀ θprev T)
{μ : MeasureTheory.Measure AmnrSpace}
(hμ : μ.AbsolutelyContinuous (MeasureTheory.volume.restrict (Set.Ioi 0 ×ˢ Set.univ)))
{S H G Ccoeff Cb Cd : ℝ}
(hS : 0 < S)
(hH : 0 < H)
(hG : 0 ≤ G)
(hC : 0 ≤ Ccoeff)
(hCb : 0 ≤ Cb)
(hCd : 0 ≤ Cd)
(hRate : κprev * S ^ 2 ≤ Cd * H)
(hAb :
∀ (j p : Fin 2) (w : List (Option (Fin 2))),
IsAmnrMixedWord w →
amnrBudget w ≤ Nstar β →
∀ (z : AmnrSpace),
|amnrWord (fun (y : AmnrSpace) => streamVel (Φ (m - 1)) y.1 y.2) w
(amnrTemperatureCoefficient I hΦ m κm κprev j p) z| ≤ Ccoeff * κprev * amnrWeight S H w)
(hBb :
∀ (q p : Fin 2) (α : List (Fin 2)) (n : ℕ),
α.length + 2 * n + 2 ≤ Nstar β →
∀ (z : AmnrSpace),
|amnrWord (fun (y : AmnrSpace) => streamVel (Φ (m - 1)) y.1 y.2) (amnrMixedWord α n)
(amnrVelocityGradient (fun (y : AmnrSpace) => streamVel (Φ (m - 1)) y.1 y.2) q p) z| ≤ Cb * H * amnrWeight S H (amnrMixedWord α n))
(hbase :
∀ i ≤ Nstar β,
∀ (p : Fin 2) (α : List (Fin 2)),
α.length ≤ Nstar β →
MeasureTheory.eLpNorm
(amnrWord (fun (y : AmnrSpace) => streamVel (Φ (m - 1)) y.1 y.2) (List.map some α) (amnrTGradient (T i) p))
2 μ ≤ ENNReal.ofReal (G * S ^ α.length))
:
have N := Nstar β;
have K := amnrNormalOrderConstant N Cb N * ↑(amnrCanonicalSamples N N).card;
have R := 1 + 2 * Cd * K * (1 + 2 ^ (N + 1) * Ccoeff) + 2 ^ (N + 1) * Cb;
∀ (r i : ℕ),
i ≤ N →
∀ (p : Fin 2) (α : List (Fin 2)),
α.length + 2 * r ≤ N →
MeasureTheory.eLpNorm
(amnrWord (fun (y : AmnrSpace) => streamVel (Φ (m - 1)) y.1 y.2) (amnrMixedWord α r)
(amnrTGradient (T i) p))
2 μ ≤ ENNReal.ofReal (R ^ r * G * amnrWeight S H (amnrMixedWord α r))
Primitive coefficient jets and proved spatial gradient jets imply all material levels. Every flux consumes only a strictly lower material level, including when its preceding iterate has a larger construction index.