The lower-order Faà di Bruno term in the flow induction

This module isolates the one-block term in the ordered-finpartition chain rule. The remaining terms are bounded by the all-order 10421 resummation, with the paper's coefficient and radius factors.

def AVenhance.FaaDiBruno.Remainder.flowSingleBlock {n : ℕ} (hn : 0 < n) : OrderedFinpartition n

The unique ordered finpartition with one block.

Equations

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

theorem AVenhance.FaaDiBruno.Remainder.flowSingleBlock_unique {n : ℕ} (hn : 0 < n) (c : OrderedFinpartition n) (hc : c.length = 1) : c = flowSingleBlock hn

theorem AVenhance.FaaDiBruno.Remainder.flowSingleBlock_compAlong_apply {n : ℕ} (hn : 0 < n) {E : Type u_1} {F : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] (q : FormalMultilinearSeries ℝ F G) (p : FormalMultilinearSeries ℝ E F) (v : Fin n → E) : (q.compAlongOrderedFinpartition p (flowSingleBlock hn)) v = (q 1) fun (x : Fin 1) => (p n) v

theorem AVenhance.FaaDiBruno.Remainder.flowPartSize_sum {n : ℕ} (c : OrderedFinpartition n) : ∑ i : Fin c.length, c.partSize i = n

theorem AVenhance.FaaDiBruno.Remainder.flowOneAddSum_le_prodAddOne {α : Type u_1} (s : Finset α) (f : α → ℕ) : 1 + ∑ i ∈ s, f i ≤ ∏ i ∈ s, (f i + 1)

theorem AVenhance.FaaDiBruno.Remainder.flowShiftFactor {n : ℕ} (hn : 0 < n) (c : OrderedFinpartition n) : (↑n + 1) ^ 2 ≤ (↑c.length + 1) ^ 2 * ∏ i : Fin c.length, (↑(c.partSize i) + 1) ^ 2

noncomputable def AVenhance.FaaDiBruno.flowPositivePartitionWeight {n : ℕ} (c : OrderedFinpartition n) : ℝ

The positive coefficient weight corresponding to an ordered finpartition in the flow induction.

Equations

• AVenhance.FaaDiBruno.flowPositivePartitionWeight c = ↑c.length.factorial * ∏ i : Fin c.length, ↑(c.partSize i).factorial * AVenhance.FaaDiBruno.flowHalfBinomialCoeff (c.partSize i - 1)

theorem AVenhance.FaaDiBruno.flowHalfCoeff_nonneg_of_posSize {r : ℕ} (hr : 1 ≤ r) : 0 ≤ flowHalfBinomialCoeff (r - 1)

theorem AVenhance.FaaDiBruno.Remainder.flowHalfBinomialBlockWeight_eq_signedPositive (r : ℕ) (hr : 1 ≤ r) : orderedPartitionHalfBinomialBlockWeight r = (-1) ^ (r - 1) * ↑r.factorial * flowHalfBinomialCoeff (r - 1)

theorem AVenhance.FaaDiBruno.Remainder.flowSignedPartitionWeight_eq_positive {n : ℕ} (c : OrderedFinpartition n) : (-1) ^ n * orderedPartitionHalfBinomialWeight c = flowPositivePartitionWeight c

theorem AVenhance.FaaDiBruno.orderedFinpartitionPositiveHalfBinomialResummation10421 (n : ℕ) : ∑ c : OrderedFinpartition n, flowPositivePartitionWeight c = 2 * ↑(n + 1).factorial * flowHalfBinomialCoeff n

The positive form of the 10421 resummation. Each summand is the absolute value of the signed paper summand, written with the positive coefficients flowHalfBinomialCoeff; this form is convenient for bounding the lower-order Faà di Bruno terms.

theorem AVenhance.FaaDiBruno.Remainder.flowVecOneEquivSymm_norm_le : ‖↑(vecOneEquiv 2).symm‖ ≤ 2

theorem AVenhance.FaaDiBruno.Remainder.flowContDiffLiftVecOneTop {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (f : Homogenization.Vec 2 → F) (hf : ContDiff ℝ (↑⊤) f) : ContDiff ℝ (↑⊤) (liftVecOne f)

theorem AVenhance.FaaDiBruno.Remainder.flowContDiffLiftVecOneEndoTop (F : Homogenization.Vec 2 → Homogenization.Vec 2) (hF : ContDiff ℝ (↑⊤) F) : ContDiff ℝ (↑⊤) (liftVecOneEndo F)

theorem AVenhance.FaaDiBruno.Remainder.flowLiftEndoDerivativeBound {m r : ℕ} (F : Homogenization.Vec 2 → Homogenization.Vec 2) (hF : ContDiff ℝ (↑m) F) (hr : r ≤ m) {C R : ℝ} (hR : 0 < R) (hC : 0 ≤ C) (hFsnorm : snorm F r R ≤ ENNReal.ofReal C) (x : Homogenization.Vec 2) : ‖iteratedFDeriv ℝ r (liftVecOneEndo F) (WithLp.toLp 1 x)‖ ≤ 2 * (C * ↑r.factorial * R ^ r / (↑r + 1) ^ 2)

theorem AVenhance.FaaDiBruno.Remainder.flowInnerCoefficientProduct {n : ℕ} (c : OrderedFinpartition n) (A : Fin c.length → ℝ) (Rf Rflow : ℝ) : ∏ i : Fin c.length, A i / Rf * ↑(c.partSize i).factorial * Rflow ^ c.partSize i / (↑(c.partSize i) + 1) ^ 2 = (∏ i : Fin c.length, A i * ↑(c.partSize i).factorial) * Rflow ^ n / (Rf ^ c.length * ∏ i : Fin c.length, (↑(c.partSize i) + 1) ^ 2)

theorem AVenhance.FaaDiBruno.Remainder.flowPartSize_lt_of_length_ge_two {n : ℕ} (c : OrderedFinpartition n) (hlen : 2 ≤ c.length) (i : Fin c.length) : c.partSize i < n

theorem AVenhance.FaaDiBruno.Remainder.flowFaaTerm_bound {N n : ℕ} (hn : 2 ≤ n) (hnN : n ≤ N) {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : Infra.Flow.SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hXsmooth : ContDiff ℝ ↑⊤ fun (p : (ℝ × Homogenization.Vec 2) × ℝ) => X p.1.1 p.1.2 p.2) {C_f R_f : ℝ} (hCf : 0 < C_f) (hRf : 0 < R_f) (hB : ∀ (t : ℝ) (k : ℕ), 1 ≤ k → k ≤ N → snorm (b t) k R_f ≤ ENNReal.ofReal C_f) (t : ℝ) (x : Homogenization.Vec 2) (hDn : ∀ (k : ℕ), 1 ≤ k → k < n → snorm (fun (y : Homogenization.Vec 2) => X t y 0) k (8 * 2 * R_f * (1 + 8 * 2 * C_f * R_f * |t|)) ≤ ENNReal.ofReal (flowHalfBinomialCoeff (k - 1) / (2 * R_f))) (c : OrderedFinpartition n) (hc : 2 ≤ c.length) : ‖(ftaylorSeries ℝ (liftVecOne (b t)) (liftVecOneEndo (fun (y : Homogenization.Vec 2) => X t y 0) (WithLp.toLp 1 x))).compAlongOrderedFinpartition (ftaylorSeries ℝ (liftVecOneEndo fun (y : Homogenization.Vec 2) => X t y 0) (WithLp.toLp 1 x)) c‖ ≤ C_f * (8 * 2 * R_f * (1 + 8 * 2 * C_f * R_f * |t|)) ^ n / (↑n + 1) ^ 2 * flowPositivePartitionWeight c

theorem AVenhance.FaaDiBruno.flowFaaRemainder_coordinate_bound {N n : ℕ} (hn : 2 ≤ n) (hnN : n ≤ N) {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : Infra.Flow.SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hXsmooth : ContDiff ℝ ↑⊤ fun (p : (ℝ × Homogenization.Vec 2) × ℝ) => X p.1.1 p.1.2 p.2) {C_f R_f : ℝ} (hCf : 0 < C_f) (hRf : 0 < R_f) (hB : ∀ (t : ℝ) (k : ℕ), 1 ≤ k → k ≤ N → snorm (b t) k R_f ≤ ENNReal.ofReal C_f) (t : ℝ) (x : Homogenization.Vec 2) (hDn : ∀ (k : ℕ), 1 ≤ k → k < n → snorm (fun (y : Homogenization.Vec 2) => X t y 0) k (8 * 2 * R_f * (1 + 8 * 2 * C_f * R_f * |t|)) ≤ ENNReal.ofReal (flowHalfBinomialCoeff (k - 1) / (2 * R_f))) (I : Fin n → Fin 2) : ‖orderedPartial n (fun (z : Homogenization.Vec 2) => b t (X t z 0)) x I - (fderiv ℝ (b t) (X t x 0)) (orderedPartial n (fun (z : Homogenization.Vec 2) => X t z 0) x I)‖ ≤ C_f * (8 * 2 * R_f * (1 + 8 * 2 * C_f * R_f * |t|)) ^ n / (↑n + 1) ^ 2 * (2 * ↑(n + 1).factorial * flowHalfBinomialCoeff n)

Pointwise bound for the lower-order part of the differentiated flow equation. The one-block Faà di Bruno term has been removed exactly; the remaining terms are summed by the positive 10421 resummation.