Positive-temperature-jet quadratic bridge. No zeroth temperature norm is used.

def AVenhance.Infra.Section5.RelativeError.PositiveTemperatureJets (A ρ S : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) : Prop

Positive spatial jets with an arbitrary amplitude on the actual T.

Equations

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

theorem AVenhance.Infra.Section5.RelativeError.fderiv_eq_zero_of_amplitude_zero {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hp : IsZ2Periodic f) {a : ℝ} (ha : 1 ≤ a) (hreg : ∀ (n : ℕ) (i : Fin n → Fin 2), 0 < n → √(l2NormSq fun (x : Homogenization.Vec 2) => (iteratedFDeriv ℝ n f x) fun (j : Fin n) => Homogenization.basisVec (i j)) ≤ 0 * ↑n.factorial * a ^ n) (v : Fin 2) (x : Homogenization.Vec 2) : (fderiv ℝ f x) (Homogenization.basisVec v) = 0

theorem AVenhance.Infra.Section5.RelativeError.relative_hasCoordinateAnalyticL1Bounds_of_bounds (A : ℝ) (hA : 1 ≤ A) : ∃ (A' : ℝ), 1 ≤ A' ∧ ∀ (S : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (ρ e : ℝ) (X : Homogenization.Vec 2 → Homogenization.Vec 2), 0 ≤ S → 0 < ρ → ρ ≤ e → e ≤ 1 → PositiveTemperatureJets A ρ S T → AnalyticBridge.FlowForErgodicBound A e X → ContDiff ℝ (↑⊤) X → ∀ t ∈ Set.Ioo 0 1, ContDiff ℝ (↑⊤) (T t) → IsZ2Periodic (T t) → ∀ (i j : Fin 2), Ergodic.HasCoordinateAnalyticL1Bounds (fun (y : Homogenization.Vec 2) => ↑(spaceGrad (T t) (X y) i * spaceGrad (T t) (X y) j)) (A' * ρ ^ (-6) * S ^ 2) (ρ / A')

Route A bridge: e.Tm.reg.upgrade (all orders, L²_x), H² ⊂ L∞, l.product, proposition 10528 and e.flow.for.ergodic give the composed L¹ analyticity required by l.flow.averages. Amplitude A' ρ^{-6} ‖θ₀‖² (so p = 6), radius ρ / A'.