One actual material gradient step from spatial orders at most two.
Step constant for spatial derivatives of the temperature material coefficient.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
AVenhance.Infra.Section5.Contracts.tMaterial_component_of_spatial_profiles
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
{m : ℕ}
(hm : 1 ≤ m)
{κm ν : ℝ}
(hκm : 0 < κm)
(hν : 0 < ν)
{g : Homogenization.Vec 2 → ℝ}
{θprev : ℝ → Homogenization.Vec 2 → ℝ}
{T : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hθ : IsClassicalSol (streamVel (Φ (m - 1))) ν (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) g θprev)
(hT : I.IsTIterates hΦ m κm ν g θprev T)
{L G CA Cb Cd : ℝ}
(hL : 0 < L)
(hG : 0 ≤ G)
(hCA : 0 ≤ CA)
(hCb : 0 ≤ Cb)
(hRate : ν * L ^ 2 ≤ Cd * a β I.Λ (m - 1))
(hCoefficient :
∀ (j p : Fin 2) (α : List (Fin 2)),
α.length ≤ 2 →
∀ (z : Section4.AmnrSpace),
|Section4.amnrWord (fun (y : Section4.AmnrSpace) => streamVel (Φ (m - 1)) y.1 y.2) (List.map some α)
(Section4.amnrTemperatureCoefficient I hΦ m κm ν j p) z| ≤ CA * ν * L ^ α.length)
(hVelocity :
∀ (q p : Fin 2) (z : Section4.AmnrSpace),
|Section4.amnrVelocityGradient (fun (y : Section4.AmnrSpace) => streamVel (Φ (m - 1)) y.1 y.2) q p z| ≤ Cb * a β I.Λ (m - 1))
(hSpatial :
∀ i ≤ Nstar β,
∀ (p : Fin 2) (α : List (Fin 2)),
α.length ≤ 2 →
MeasureTheory.eLpNorm
(Section4.amnrWord (fun (y : Section4.AmnrSpace) => streamVel (Φ (m - 1)) y.1 y.2) (List.map some α)
(Section4.amnrTGradient (T i) p))
2 (MeasureTheory.volume.restrict timeCube) ≤ ENNReal.ofReal (G * L ^ α.length))
(p : Fin 2)
:
MeasureTheory.eLpNorm
(Section4.amnrWord (fun (y : Section4.AmnrSpace) => streamVel (Φ (m - 1)) y.1 y.2) [none]
(Section4.amnrTGradient (T (Nstar β)) p))
2 (MeasureTheory.volume.restrict timeCube) ≤ ENNReal.ofReal (tMaterialSpatialStepConstant Cb CA Cd * a β I.Λ (m - 1) * G)
The local budget is exactly two. No positive material coefficient or velocity-gradient derivative is among the hypotheses.