Hölder bound of the tail piece w = θ − θ_M

Uniform in κ and M: ‖w(t) − w(s)‖ ≤ K_w ‖θ₀‖_{H¹} |t − s|^{μ_w}.

noncomputable def AVenhance.Infra.FullTheorem.tailExp (β : ℝ) : ℝ

The exponent a = qβ − (β − γ) of the tail decay.

Equations

• AVenhance.Infra.FullTheorem.tailExp β = AVenhance.q β * β - (β - AVenhance.gamma β)

theorem AVenhance.Infra.FullTheorem.tailExp_pos {β : ℝ} (hβ : 1 < β) (hβ' : β < 4 / 3) : 0 < tailExp β

noncomputable def AVenhance.Infra.FullTheorem.tailMu (β : ℝ) : ℝ

The Hölder exponent of the tail piece.

Equations

• AVenhance.Infra.FullTheorem.tailMu β = AVenhance.Infra.FullTheorem.lebronMu (AVenhance.Infra.FullTheorem.tailExp β) (β - AVenhance.gamma β)

noncomputable def AVenhance.Infra.FullTheorem.tailK (β CU Ct Bm : ℝ) : ℝ

The constant of the tail piece.

Equations

• One or more equations did not get rendered due to their size.

theorem AVenhance.Infra.FullTheorem.tailK_nonneg {β : ℝ} (hβ : 1 < β) (hβ' : β < 4 / 3) {CU Ct Bm : ℝ} (hCU : 0 ≤ CU) (hCt : 0 ≤ Ct) (hBm : 0 ≤ Bm) : 0 ≤ tailK β CU Ct Bm

theorem AVenhance.Infra.FullTheorem.w_holder {β CU Ct Bφ : ℝ} (hU : LemmaUWith CU) (hCU : 0 < CU) (hCt : 0 ≤ Ct) (hBφ : 0 ≤ Bφ) {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {φ : ℝ → Homogenization.Vec 2 → ℝ} (htail : ∀ (M : ℕ) (t : ℝ) (x : Homogenization.Vec 2), |φ t x - Φ M t x| ≤ Ct * epsilon β I.Λ (M + 1) ^ β) (hφ_meas : MeasureTheory.AEStronglyMeasurable (fun (p : ℝ × Homogenization.Vec 2) => φ p.1 p.2) (MeasureTheory.volume.restrict (Set.Icc 0 1 ×ˢ Set.univ))) (hφ_per : ∀ t ∈ Set.Icc 0 1, IsZ2Periodic (φ t)) (hφ_diff : ∀ t ∈ Set.Icc 0 1, Differentiable ℝ (φ t)) (hb_meas : MeasureTheory.AEStronglyMeasurable (fun (p : ℝ × Homogenization.Vec 2) => streamVel φ p.1 p.2) (MeasureTheory.volume.restrict (Set.Icc 0 1 ×ˢ Set.univ))) (hb_per : ∀ t ∈ Set.Icc 0 1, IsZ2Periodic (streamVel φ t)) (hdiv : IsDivFree (streamVel φ)) (hb_bdd : ∀ t ∈ Set.Icc 0 1, ∀ (x : Homogenization.Vec 2), ‖streamVel φ t x‖ ≤ Bφ) {κ : ℝ} {M : ℕ} (hM : 1 ≤ M) (hκlo : 1 / 2 * epsilon β I.Λ M ^ (β - gamma β) ≤ κ) (hκ1 : κ ≤ 1) {θ₀ : Homogenization.Vec 2 → ℝ} (hθ₀ : ContDiff ℝ (↑⊤) θ₀) (hper : IsZ2Periodic θ₀) {θ : ℝ → Homogenization.Vec 2 → ℝ} (hθ : IsWeakSolution (streamVel φ) κ θ₀ θ) {θM : ℝ → Homogenization.Vec 2 → ℝ} (hθM : IsClassicalSol (streamVel (Φ M)) κ (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θM) : IsHolderTimeL2 (tailMu β) (tailK β CU Ct (max Bφ (velBound β)) * √(l2NormSq θ₀ + gradNormSq (spaceGrad θ₀))) fun (t : ℝ) (x : Homogenization.Vec 2) => θ t x - θM t x