Primitive regularity and lower flux jets for the actual iterate family.
theorem
AVenhance.Infra.Section4.amnr_tIterates_gradient_smooth
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
{m : ℕ}
{κm κ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)
(i : ℕ)
(hi : i ≤ Nstar β)
(p : Fin 2)
:
ContDiffOn ℝ (↑⊤) (amnrTGradient (T i) p) (Set.Ioi 0 ×ˢ Set.univ)
theorem
AVenhance.Infra.Section4.amnr_tIterates_flux_smooth
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
{m : ℕ}
(hm : 1 ≤ m)
{κm κprev : ℝ}
(hκm : 0 < κm)
{θ₀ : 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)
(i : ℕ)
(hi : i ≤ Nstar β)
(q : Fin 2)
:
ContDiffOn ℝ (↑(Nstar β)) (amnrIterateFlux I hΦ m κm κprev T i q) (Set.Ioi 0 ×ˢ Set.univ)
theorem
AVenhance.Infra.Section4.amnr_tIterates_flux_mixed_bound_of_lower_gradients
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
{m : ℕ}
(hm : 1 ≤ m)
{κm κprev : ℝ}
(hκm : 0 < κm)
{θ₀ : 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 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 : AmnrSpace),
|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 :
∀ i ≤ Nstar β,
∀ (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 (T i) p))
2 μ ≤ ENNReal.ofReal (G * amnrWeight S H (amnrMixedWord α r)))
(i : ℕ)
(hi : i ≤ Nstar β)
(q : Fin 2)
(α : List (Fin 2))
(r : ℕ)
(hbudget : α.length + 2 * r ≤ Nstar β)
(hr : r ≤ cut)
:
MeasureTheory.eLpNorm
(amnrWord (fun (y : AmnrSpace) => streamVel (Φ (m - 1)) y.1 y.2) (amnrMixedWord α r)
(amnrIterateFlux I hΦ m κm κprev T i q))
2 μ ≤ ENNReal.ofReal (2 ^ (Nstar β + 1) * A * G * amnrWeight S H (amnrMixedWord α r))
Only lower material levels of the preceding temperature enter a flux jet. Both the zero starting flux and every forced flux are derived from the construction.