Amplitude-generic adapters for the mixed temperature/material calculus.
The rate variables below are deliberately named L and Q: in the AMNR engine they are the spatial and material rates, while the separate G is the temperature-gradient amplitude.
theorem
AVenhance.Infra.Section5.RelativeError.relative_mixed_material_jets_of_source_profiles
{β : ℝ}
(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 Section4.AmnrSpace}
(hμ : μ.AbsolutelyContinuous (MeasureTheory.volume.restrict (Set.Ioi 0 ×ˢ Set.univ)))
{L Q G Ccoeff Cb Cd : ℝ}
(hL : 0 < L)
(hQ : 0 < Q)
(hG : 0 ≤ G)
(hCcoeff : 0 ≤ Ccoeff)
(hCb : 0 ≤ Cb)
(hCd : 0 ≤ Cd)
(hRate : κprev * L ^ 2 ≤ Cd * Q)
(hCoefficient :
∀ (j p : Fin 2) (w : List (Option (Fin 2))),
Section4.IsAmnrMixedWord w →
Section4.amnrBudget w ≤ Nstar β →
∀ (z : Section4.AmnrSpace),
|Section4.amnrWord (fun (y : Section4.AmnrSpace) => streamVel (Φ (m - 1)) y.1 y.2) w
(Section4.amnrTemperatureCoefficient I hΦ m κm κprev j p) z| ≤ Ccoeff * κprev * Section4.amnrWeight L Q w)
(hVelocityGradient :
∀ (q p : Fin 2) (α : List (Fin 2)) (n : ℕ),
α.length + 2 * n + 2 ≤ Nstar β →
∀ (z : Section4.AmnrSpace),
|Section4.amnrWord (fun (y : Section4.AmnrSpace) => streamVel (Φ (m - 1)) y.1 y.2) (Section4.amnrMixedWord α n)
(Section4.amnrVelocityGradient (fun (y : Section4.AmnrSpace) => streamVel (Φ (m - 1)) y.1 y.2) q p) z| ≤ Cb * Q * Section4.amnrWeight L Q (Section4.amnrMixedWord α n))
(hSpatialGradient :
∀ i ≤ Nstar β,
∀ (p : Fin 2) (α : List (Fin 2)),
α.length ≤ Nstar β →
MeasureTheory.eLpNorm
(Section4.amnrWord (fun (y : Section4.AmnrSpace) => streamVel (Φ (m - 1)) y.1 y.2) (List.map some α)
(Section4.amnrTGradient (T i) p))
2 μ ≤ ENNReal.ofReal (G * L ^ α.length))
:
have N := Nstar β;
have K := Section4.amnrNormalOrderConstant N Cb N * ↑(Section4.amnrCanonicalSamples N N).card;
have Cmix := 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
(Section4.amnrWord (fun (y : Section4.AmnrSpace) => streamVel (Φ (m - 1)) y.1 y.2)
(Section4.amnrMixedWord α r) (Section4.amnrTGradient (T i) p))
2 μ ≤ ENNReal.ofReal (Cmix ^ r * G * Section4.amnrWeight L Q (Section4.amnrMixedWord α r))
Apply the mixed AMNR induction to the actual terminal iterate, keeping an arbitrary gradient amplitude and keeping the two derivative rates separate. The three quantitative inputs are the source coefficient, flow-gradient and positive spatial-gradient bounds; the conclusion is the full mixed-word profile used by the later RelativeError material adapters.