Actual canonical temperature flux jets at the finite source budget.
noncomputable def
AVenhance.Infra.Section4.amnrTemperatureFlux
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
(m : ℕ)
(κm κprev : ℝ)
(u : ℝ → Homogenization.Vec 2 → ℝ)
(j : Fin 2)
(z : AmnrSpace)
:
Temperature gradient contracted with the temperature coefficient matrix.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
AVenhance.Infra.Section4.amnr_temperatureFlux_mixed_bound_of_gradients
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
{m : ℕ}
(hm : 1 ≤ m)
{κm κprev : ℝ}
(hκm : 0 < κm)
{F u : ℝ → Homogenization.Vec 2 → ℝ}
{u₀ : Homogenization.Vec 2 → ℝ}
(hu : IsClassicalSol (streamVel (Φ (m - 1))) κprev F u₀ u)
{U : Set AmnrSpace}
(hU : IsOpen U)
(hUpos : U ⊆ Set.Ioi 0 ×ˢ Set.univ)
{μ : MeasureTheory.Measure AmnrSpace}
(hμ : μ.AbsolutelyContinuous (MeasureTheory.volume.restrict U))
{S H A G : ℝ}
(hS : 0 ≤ S)
(hH : 0 ≤ H)
(hA : 0 ≤ A)
(hG : 0 ≤ G)
{cut : ℕ}
(hAb :
∀ (j p : Fin 2) (v : List (Option (Fin 2))),
IsAmnrMixedWord v →
amnrBudget v ≤ Nstar β →
∀ z ∈ U,
|amnrWord (fun (y : AmnrSpace) => streamVel (Φ (m - 1)) y.1 y.2) v
(amnrTemperatureCoefficient I hΦ m κm κprev j p) z| ≤ A * amnrWeight S H v)
(hgb :
∀ (p : Fin 2) (α : List (Fin 2)) (r : ℕ),
α.length + 2 * r ≤ Nstar β →
r ≤ cut →
MeasureTheory.eLpNorm
(amnrWord (fun (y : AmnrSpace) => streamVel (Φ (m - 1)) y.1 y.2) (amnrMixedWord α r) (amnrTGradient u p)) 2
μ ≤ ENNReal.ofReal (G * amnrWeight S H (amnrMixedWord α r)))
(j : Fin 2)
(α : List (Fin 2))
(r : ℕ)
(hbudget : α.length + 2 * r ≤ Nstar β)
(hcut : r ≤ cut)
:
MeasureTheory.eLpNorm
(amnrWord (fun (y : AmnrSpace) => streamVel (Φ (m - 1)) y.1 y.2) (amnrMixedWord α r)
(amnrTemperatureFlux I hΦ m κm κprev u j))
2 μ ≤ ENNReal.ofReal (2 ^ (Nstar β + 1) * A * G * amnrWeight S H (amnrMixedWord α r))
The canonical flux estimate is an actual finite Leibniz contraction. This conditional calculus helper takes lower temperature jets, leaving their PDE induction as a separate source proof.