Transport Sharp Estimate

Support for the Armstrong–Vicol anomalous-diffusion formalization.

noncomputable def AVenhance.FaaDiBruno.transportSharpLowerCoefficient (n k : ℕ) (C_f C_g R : ℝ) : ℝ

Coefficient of a lower-order term in the sharp transport majorant.

Equations

• AVenhance.FaaDiBruno.transportSharpLowerCoefficient n k C_f C_g R = ↑(n.choose k) * (C_f * ↑(n - k).factorial * R ^ (n - k) / (↑n - ↑k + 1) ^ 2) * (16 * C_g * ↑(k + 1).factorial / (↑k + 2) ^ 2)

noncomputable def AVenhance.FaaDiBruno.transportSharpLowerIntegrand (n k : ℕ) (C_f C_g R s : ℝ) : ℝ

Time-dependent integrand for a lower-order sharp transport contribution.

Equations

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

noncomputable def AVenhance.FaaDiBruno.transportSharpSourceMajorant (n : ℕ) (C_f C_g R S s : ℝ) : ℝ

Scalar majorant for the source term in the sharp transport estimate.

Equations

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

theorem AVenhance.FaaDiBruno.TransportSharpEstimate.choose_factorials_succ_product {n k : ℕ} (hk : k ≤ n) : ↑(n.choose k) * ↑(n - k).factorial * ↑(k + 1).factorial = ↑n.factorial * (↑k + 1)

theorem AVenhance.FaaDiBruno.TransportSharpEstimate.transportLowerIntegralTerm_bound {n k : ℕ} (hk : k < n - 1) {C_f C_g R ρ t : ℝ} (hCf : 0 < C_f) (hCg : 0 ≤ C_g) (hR : 0 < R) (ht : 0 ≤ t) (hρ : R ≤ ρ) : 2 * (↑(n.choose k) * (C_f * ↑(n - k).factorial * R ^ (n - k) / (↑n - ↑k + 1) ^ 2) * (16 * C_g * ↑(k + 1).factorial / (↑k + 2) ^ 2) * (t * ρ ^ (k + 2) / (8 * C_f * R ^ 2 * (↑k + 2)))) ≤ t * (↑n.factorial * ρ ^ n / (↑n + 1) ^ 2) * (4 * C_g * (↑n + 1) ^ 2 / ((↑n - ↑k + 1) ^ 2 * (↑k + 2) ^ 2))

theorem AVenhance.FaaDiBruno.transportSharpSourceMajorant_integral_bound {n : ℕ} (hn : 2 ≤ n) {C_f C_g R S t : ℝ} (hCf : 0 < C_f) (hCg : 0 ≤ C_g) (hR : 0 < R) (hS : 0 ≤ S) (ht : 0 ≤ t) (hT : t ≤ 1 / (8 * C_f * R)) : ∫ (s : ℝ) in 0..t, transportSharpSourceMajorant n C_f C_g R S s ≤ t * (↑n.factorial * transportShiftRadius C_f R t ^ n / (↑n + 1) ^ 2) * (C_g + S / 8 + 12 * C_g)

Integrating the sharp source majorant over a characteristic gives the equal-radius feedback coefficient and the corrected shifted convolution.

theorem AVenhance.FaaDiBruno.transportSolution_snorm_order_equalRadius {n : ℕ} (hn : 2 ≤ n) {b g Y : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hY : IsClassicalTransportSolution b g Y) (hb : ContDiff ℝ (↑⊤) (Function.uncurry b)) (hg : ContDiff ℝ (↑⊤) (Function.uncurry g)) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) {C_f C_g R : ℝ} (hCf : 0 < C_f) (hCg : 0 ≤ C_g) (hR : 0 < R) (hB : ∀ (t : ℝ) (m : ℕ), 1 ≤ m → m ≤ n → snorm (b t) m R ≤ ENNReal.ofReal C_f) (hG : ∀ (t : ℝ), snorm (g t) n R ≤ ENNReal.ofReal C_g) (hLower : ∀ (k : ℕ), 1 ≤ k → k < n → ∀ (t : ℝ), |t| ≤ 1 / (8 * C_f * R) → snorm (Y t) k (transportShiftRadius C_f R |t|) ≤ ENNReal.ofReal (16 * C_g * |t|)) (t : ℝ) : |t| ≤ 1 / (8 * C_f * R) → snorm (Y t) n (transportShiftRadius C_f R |t|) ≤ ENNReal.ofReal (16 * C_g * |t|)

The corrected equal-radius, dimension-two form of Lemma 10577 at order n ≥ 2. The lower orders are the induction hypotheses on the same shifted radius, and the top-order feedback is absorbed with the corrected factor.

theorem AVenhance.FaaDiBruno.transportSolution_snorm_equalRadius_one {N : ℕ} (hN : 1 ≤ N) {b g Y : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hY : IsClassicalTransportSolution b g Y) (hb : ContDiff ℝ (↑⊤) (Function.uncurry b)) (hg : ContDiff ℝ (↑⊤) (Function.uncurry g)) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) {C_f C_g R : ℝ} (hCf : 0 < C_f) (hCg : 0 ≤ C_g) (hR : 0 < R) (hB : ∀ (t : ℝ) (m : ℕ), 1 ≤ m → m ≤ N → snorm (b t) m R ≤ ENNReal.ofReal C_f) (hG : ∀ (t : ℝ) (m : ℕ), 1 ≤ m → m ≤ N → snorm (g t) m R ≤ ENNReal.ofReal C_g) {t : ℝ} (ht : |t| ≤ 1 / (8 * C_f * R)) : snorm (Y t) 1 (transportShiftRadius C_f R |t|) ≤ ENNReal.ofReal (16 * C_g * |t|)

The order-one base case with finite-order coefficient bounds.

theorem AVenhance.FaaDiBruno.transportSolution_snorm_equalRadius_step {n N : ℕ} (hn : 2 ≤ n) (hnN : n ≤ N) {b g Y : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hY : IsClassicalTransportSolution b g Y) (hb : ContDiff ℝ (↑⊤) (Function.uncurry b)) (hg : ContDiff ℝ (↑⊤) (Function.uncurry g)) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) {C_f C_g R : ℝ} (hCf : 0 < C_f) (hCg : 0 ≤ C_g) (hR : 0 < R) (hB : ∀ (t : ℝ) (m : ℕ), 1 ≤ m → m ≤ N → snorm (b t) m R ≤ ENNReal.ofReal C_f) (hG : ∀ (t : ℝ) (m : ℕ), 1 ≤ m → m ≤ N → snorm (g t) m R ≤ ENNReal.ofReal C_g) (hLower : ∀ (k : ℕ), 1 ≤ k → k < n → ∀ (t : ℝ), |t| ≤ 1 / (8 * C_f * R) → snorm (Y t) k (transportShiftRadius C_f R |t|) ≤ ENNReal.ofReal (16 * C_g * |t|)) {t : ℝ} (ht : |t| ≤ 1 / (8 * C_f * R)) : snorm (Y t) n (transportShiftRadius C_f R |t|) ≤ ENNReal.ofReal (16 * C_g * |t|)

The induction step in Lemma 10577, isolated so each high-order estimate elaborates under Lean's default heartbeat budget.

theorem AVenhance.FaaDiBruno.transportSolution_snorm_equalRadius_all {N : ℕ} {b g Y : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hY : IsClassicalTransportSolution b g Y) (hb : ContDiff ℝ (↑⊤) (Function.uncurry b)) (hg : ContDiff ℝ (↑⊤) (Function.uncurry g)) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) {C_f C_g R : ℝ} (hCf : 0 < C_f) (hCg : 0 ≤ C_g) (hR : 0 < R) (hB : ∀ (t : ℝ) (m : ℕ), 1 ≤ m → m ≤ N → snorm (b t) m R ≤ ENNReal.ofReal C_f) (hG : ∀ (t : ℝ) (m : ℕ), 1 ≤ m → m ≤ N → snorm (g t) m R ≤ ENNReal.ofReal C_g) (n : ℕ) : 1 ≤ n → n ≤ N → ∀ (t : ℝ), |t| ≤ 1 / (8 * C_f * R) → snorm (Y t) n (transportShiftRadius C_f R |t|) ≤ ENNReal.ofReal (16 * C_g * |t|)

All positive spatial orders through the paper's finite cutoff in the corrected equal-radius form of Lemma 10577. The induction hypotheses use the shifted radius at each time, so the lower-order terms in the differentiated equation are exactly those absorbed by the corrections.

theorem AVenhance.FaaDiBruno.transportSolution_gradient_snorm_equalRadius {N n : ℕ} (hn : n + 1 ≤ N) {b g Y : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hY : IsClassicalTransportSolution b g Y) (hb : ContDiff ℝ (↑⊤) (Function.uncurry b)) (hg : ContDiff ℝ (↑⊤) (Function.uncurry g)) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) {C_f C_g R : ℝ} (hCf : 0 < C_f) (hCg : 0 ≤ C_g) (hR : 0 < R) (hB : ∀ (t : ℝ) (m : ℕ), 1 ≤ m → m ≤ N → snorm (b t) m R ≤ ENNReal.ofReal C_f) (hG : ∀ (t : ℝ) (m : ℕ), 1 ≤ m → m ≤ N → snorm (g t) m R ≤ ENNReal.ofReal C_g) {t : ℝ} (ht : |t| ≤ 1 / (8 * C_f * R)) : snorm (spatialGradientMatrix (Y t)) n (R * (1 + 8 * |t| * C_f * R) ^ 2) ≤ ENNReal.ofReal (8 * C_g / C_f)

The consumed finite-order, equal-radius form of Corollary 10670. The coordinate matrix gradient is controlled through order n by Lemma 10577 at order n+1; this includes the separate n=0 endpoint.