Relative Positive Product

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section5.RelativeError.snorm_fderiv_le {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hp : IsZ2Periodic f) {B a K : ℝ} (hB : 0 ≤ B) (ha : 1 ≤ a) (hK : ∀ (n : ℕ), (↑n + 3) ^ 5 ≤ K * 2 ^ n) (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)) ≤ B * ↑n.factorial * a ^ n) (v : Fin 2) (n : ℕ) : FaaDiBruno.snorm (fun (y : Homogenization.Vec 2) => (fderiv ℝ f y) (Homogenization.basisVec v)) n (2 * a) ≤ ENNReal.ofReal (3 * AnalyticBridge.sobolevConst * B * K * a ^ 3)

Step 2: ⟦∂_v f⟧_{n,2a} ≤ 3 sc K B a³ for every order n.

theorem AVenhance.Infra.Section5.RelativeError.snormMax_fderiv_le {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hp : IsZ2Periodic f) {B a K : ℝ} (hB : 0 ≤ B) (ha : 1 ≤ a) (hK : ∀ (n : ℕ), (↑n + 3) ^ 5 ≤ K * 2 ^ n) (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)) ≤ B * ↑n.factorial * a ^ n) (v : Fin 2) (n : ℕ) : FaaDiBruno.snormMax (fun (y : Homogenization.Vec 2) => (fderiv ℝ f y) (Homogenization.basisVec v)) n (2 * a) ≤ ENNReal.ofReal (3 * AnalyticBridge.sobolevConst * B * K * a ^ 3)

snormMax of ∂_v f up to order n.

theorem AVenhance.Infra.Section5.RelativeError.snorm_fderiv_mul_le {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hp : IsZ2Periodic f) {B a K : ℝ} (hB : 0 ≤ B) (ha : 1 ≤ a) (hK : ∀ (n : ℕ), (↑n + 3) ^ 5 ≤ K * 2 ^ n) (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)) ≤ B * ↑n.factorial * a ^ n) (i j : Fin 2) (n : ℕ) : FaaDiBruno.snorm (fun (y : Homogenization.Vec 2) => (fderiv ℝ f y) (Homogenization.basisVec i) * (fderiv ℝ f y) (Homogenization.basisVec j)) n (2 * a) ≤ ENNReal.ofReal (4 * (3 * AnalyticBridge.sobolevConst * B * K * a ^ 3) ^ 2)

Step 3: ⟦∂_i f ∂_j f⟧_{n,2a} ≤ 4 C_h².