The finite generating sum for genuine derivatives. This file derives the identity-map contribution and the composition estimate needed by the flow bootstrap from actual derivatives, including the exact Faà di Bruno formula.

The finite Gevrey-two generating sum obeys an actual composition estimate. In contrast to replacing all jets by one order-dependent bound, this estimate retains the finite sum of the inner derivatives.

Finite polynomial majorants for factorial-square Taylor coefficients. The polynomials below are auxiliary nonnegative scalar polynomials. Their composition is the exact scalar Faà di Bruno sum, not an assumed majorant for a flow or for a solution of a differential equation.

theorem EulerGevreyGeneratingAlgebra.factorialProduct_nonneg {n : ℕ} (c : OrderedFinpartition n) : 0 ≤ EulerGevreyComposition.factorialProduct c

theorem EulerGevreyGeneratingAlgebra.partition_factorial_le {n : ℕ} (c : OrderedFinpartition n) : ↑c.length.factorial * EulerGevreyComposition.factorialProduct c ≤ ↑n.factorial

The factorial used by an ordered partition never exceeds the total factorial. This is the extra factor available in Gevrey order two.

theorem EulerGevreyGeneratingAlgebra.polynomial_iteratedDeriv (p : Polynomial ℝ) (n : ℕ) (x : ℝ) : iteratedDeriv n (fun (y : ℝ) => Polynomial.eval y p) x = Polynomial.eval x ((⇑Polynomial.derivative)^[n] p)

theorem EulerGevreyGeneratingAlgebra.polynomial_iteratedDeriv_zero (p : Polynomial ℝ) (n : ℕ) : iteratedDeriv n (fun (y : ℝ) => Polynomial.eval y p) 0 = ↑n.factorial * p.coeff n

theorem EulerGevreyGeneratingAlgebra.polynomial_contDiff (p : Polynomial ℝ) : ContDiff ℝ ↑⊤ fun (y : ℝ) => Polynomial.eval y p

theorem EulerGevreyGeneratingAlgebra.comp_coefficient (p q : Polynomial ℝ) (hp : p.coeff 0 = 0) (n : ℕ) : ↑n.factorial * (q.comp p).coeff n = ∑ c : OrderedFinpartition n, ↑c.length.factorial * q.coeff c.length * ∏ i : Fin c.length, ↑(c.partSize i).factorial * p.coeff (c.partSize i)

Exact coefficient version of scalar Faà di Bruno at zero.

noncomputable def EulerGevreyGeneratingAlgebra.jetPolynomial (N : ℕ) (a : ℕ → ℝ) : Polynomial ℝ

A finite scalar polynomial whose constant coefficient is zero.

Equations

• EulerGevreyGeneratingAlgebra.jetPolynomial N a = ∑ j ∈ Finset.Icc 1 N, (Polynomial.monomial j) (a j)

theorem EulerGevreyGeneratingAlgebra.jetPolynomial_coeff (N : ℕ) (a : ℕ → ℝ) (j : ℕ) : (jetPolynomial N a).coeff j = if j ∈ Finset.Icc 1 N then a j else 0

@[simp]

theorem EulerGevreyGeneratingAlgebra.jetPolynomial_zero (N : ℕ) (a : ℕ → ℝ) : (jetPolynomial N a).coeff 0 = 0

theorem EulerGevreyGeneratingAlgebra.jetPolynomial_coeff_of_mem (N : ℕ) (a : ℕ → ℝ) (j : ℕ) (hj : j ∈ Finset.Icc 1 N) : (jetPolynomial N a).coeff j = a j

theorem EulerGevreyGeneratingAlgebra.jetPolynomial_eval (N : ℕ) (a : ℕ → ℝ) (x : ℝ) : Polynomial.eval x (jetPolynomial N a) = ∑ j ∈ Finset.Icc 1 N, a j * x ^ j

def EulerGevreyGeneratingAlgebra.NonnegativeCoefficients (p : Polynomial ℝ) : Prop

Nonnegative coefficients, given by ∀ n, 0 ≤ p.coeff n.

Equations

• EulerGevreyGeneratingAlgebra.NonnegativeCoefficients p = ∀ (n : ℕ), 0 ≤ p.coeff n

theorem EulerGevreyGeneratingAlgebra.jetPolynomial_nonnegative (N : ℕ) (a : ℕ → ℝ) (ha : ∀ j ∈ Finset.Icc 1 N, 0 ≤ a j) : NonnegativeCoefficients (jetPolynomial N a)

theorem EulerGevreyGeneratingAlgebra.nonnegative_mul {p q : Polynomial ℝ} (hp : NonnegativeCoefficients p) (hq : NonnegativeCoefficients q) : NonnegativeCoefficients (p * q)

theorem EulerGevreyGeneratingAlgebra.nonnegative_pow {p : Polynomial ℝ} (hp : NonnegativeCoefficients p) (n : ℕ) : NonnegativeCoefficients (p ^ n)

theorem EulerGevreyGeneratingAlgebra.nonnegative_comp {p q : Polynomial ℝ} (hp : NonnegativeCoefficients p) (hq : NonnegativeCoefficients q) : NonnegativeCoefficients (q.comp p)

theorem EulerGevreyGeneratingAlgebra.coefficient_sum_le_eval (p : Polynomial ℝ) (hp : NonnegativeCoefficients p) (s : Finset ℕ) (x : ℝ) (hx : 0 ≤ x) : ∑ j ∈ s, p.coeff j * x ^ j ≤ Polynomial.eval x p

A partial sum of a nonnegative polynomial is bounded by its actual evaluation. No bound on the degree of the composed polynomial is needed.

theorem EulerGevreyGeneratingComposition.norm_taylorComp_le_coefficient {E : Type u_1} {F : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] (P : FormalMultilinearSeries ℝ E F) (Q : FormalMultilinearSeries ℝ F G) (p q : Polynomial ℝ) (hp0 : p.coeff 0 = 0) (hp : EulerGevreyGeneratingAlgebra.NonnegativeCoefficients p) (hq : EulerGevreyGeneratingAlgebra.NonnegativeCoefficients q) (n : ℕ) (hn : 0 < n) (hP : ∀ (j : ℕ), 0 < j → j ≤ n → ‖P j‖ ≤ ↑j.factorial ^ 2 * p.coeff j) (hQ : ∀ (j : ℕ), 0 < j → j ≤ n → ‖Q j‖ ≤ ↑j.factorial ^ 2 * q.coeff j) : ‖Q.taylorComp P n‖ ≤ ↑n.factorial ^ 2 * (q.comp p).coeff n

Comparison with an exact scalar polynomial composition.

theorem EulerGevreyGeneratingComposition.generating_sum_le_polynomial {E : Type u_1} {F : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] (P : FormalMultilinearSeries ℝ E F) (Q : FormalMultilinearSeries ℝ F G) (N : ℕ) (a b : ℕ → ℝ) (ha : ∀ j ∈ Finset.Icc 1 N, 0 ≤ a j) (hb : ∀ j ∈ Finset.Icc 1 N, 0 ≤ b j) (hP : ∀ j ∈ Finset.Icc 1 N, ‖P j‖ ≤ ↑j.factorial ^ 2 * a j) (hQ : ∀ j ∈ Finset.Icc 1 N, ‖Q j‖ ≤ ↑j.factorial ^ 2 * b j) (z : ℝ) (hz : 0 ≤ z) : ∑ n ∈ Finset.Icc 1 N, ‖Q.taylorComp P n‖ / ↑n.factorial ^ 2 * z ^ n ≤ Polynomial.eval (Polynomial.eval z (EulerGevreyGeneratingAlgebra.jetPolynomial N a)) (EulerGevreyGeneratingAlgebra.jetPolynomial N b)

Finite sums are bounded by evaluating the composed nonnegative polynomial. No derivative beyond order N occurs.

noncomputable def EulerGevreyGeneratingComposition.normalizedJet {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (P : FormalMultilinearSeries ℝ E F) (n : ℕ) : ℝ

Normalized jet, given by ‖P n‖/(n.factorial : ℝ)^2.

Equations

• EulerGevreyGeneratingComposition.normalizedJet P n = ‖P n‖ / ↑n.factorial ^ 2

noncomputable def EulerGevreyGeneratingComposition.generatingSum {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (P : FormalMultilinearSeries ℝ E F) (N : ℕ) (z : ℝ) : ℝ

Generating sum, given by ∑ n ∈ Finset.Icc 1 N, normalizedJet P n*z^n.

Equations

• EulerGevreyGeneratingComposition.generatingSum P N z = ∑ n ∈ Finset.Icc 1 N, EulerGevreyGeneratingComposition.normalizedJet P n * z ^ n

theorem EulerGevreyGeneratingComposition.generatingSum_nonneg {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (P : FormalMultilinearSeries ℝ E F) (N : ℕ) (z : ℝ) (hz : 0 ≤ z) : 0 ≤ generatingSum P N z

theorem EulerGevreyGeneratingComposition.generatingSum_taylorComp_le {E : Type u_1} {F : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] (P : FormalMultilinearSeries ℝ E F) (Q : FormalMultilinearSeries ℝ F G) (N : ℕ) (B R z : ℝ) (hB : 0 ≤ B) (hR : 0 ≤ R) (hz : 0 ≤ z) (hQ : ∀ j ∈ Finset.Icc 1 N, ‖Q j‖ ≤ B * R ^ j * ↑j.factorial ^ 2) (hsmall : R * generatingSum P N z < 1) : generatingSum (Q.taylorComp P) N z ≤ B * (R * generatingSum P N z) / (1 - R * generatingSum P N z)

The nonlinear generating-function bound needed for the small-flow bootstrap. The inner generating sum is retained without a radius loss.

The finite generating-sum bootstrap used for the small lifted flow in source (21). A first-hitting argument proves the bound from an integral inequality valid only inside its radius of convergence. No global smallness of the unknown path or exponential flow bound is assumed.

theorem EulerGevreyFlowBootstrap.continuous_barrier (f : ℝ → ℝ) (T B a : ℝ) (_hT : 0 ≤ T) (hB : 0 ≤ B) (ha : 0 < a) (hBa : B * T < a) (hf : ContinuousOn f (Set.Icc 0 T)) (hf0 : f 0 = 0) (hstep : ∀ t ∈ Set.Icc 0 T, (∀ s ∈ Set.Icc 0 t, f s ≤ a) → f t ≤ B * t) (t : ℝ) : t ∈ Set.Icc 0 T → f t ≤ B * t

A continuous path cannot first hit a barrier if its bound up to that first hit lies strictly below the barrier.

noncomputable def EulerGevreyFlowBootstrap.rationalRate (B R a u : ℝ) : ℝ

Rational rate, given by B*(R*(a+u))/(1-R*(a+u)).

Equations

• EulerGevreyFlowBootstrap.rationalRate B R a u = B * (R * (a + u)) / (1 - R * (a + u))

theorem EulerGevreyFlowBootstrap.rationalRate_le (B R a u : ℝ) (hB : 0 ≤ B) (hu : R * (a + u) ≤ 1 / 2) : rationalRate B R a u ≤ B

theorem EulerGevreyFlowBootstrap.rational_integral_bootstrap (f : ℝ → ℝ) (T B R : ℝ) (hT : 0 ≤ T) (hB : 0 ≤ B) (hR : 0 < R) (hsmall : B * R * T ≤ 1 / 8) (hf : ContinuousOn f (Set.Icc 0 T)) (hf0 : f 0 = 0) (hineq : ∀ t ∈ Set.Icc 0 T, (∀ s ∈ Set.Icc 0 t, R * ((4 * R)⁻¹ + f s) ≤ 1 / 2) → f t ≤ ∫ (s : ℝ) in 0..t, rationalRate B R (4 * R)⁻¹ (f s)) (t : ℝ) : t ∈ Set.Icc 0 T → f t ≤ B * t ∧ R * ((4 * R)⁻¹ + f t) ≤ 3 / 8

The nonlinear generating-sum inequality closes at BRT≤1/8. The bound is linear in the velocity size B and time, with no exponential factor.

noncomputable def EulerGevreyGeneratingDerivatives.derivativeSum {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : E → F) (N : ℕ) (z : ℝ) (x : E) : ℝ

Derivative sum, given by generatingSum (ftaylorSeries ℝ f x) N z.

Equations

• EulerGevreyGeneratingDerivatives.derivativeSum f N z x = EulerGevreyGeneratingComposition.generatingSum (ftaylorSeries ℝ f x) N z

theorem EulerGevreyGeneratingDerivatives.derivativeSum_nonneg {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : E → F) (N : ℕ) (z : ℝ) (x : E) (hz : 0 ≤ z) : 0 ≤ derivativeSum f N z x

theorem EulerGevreyGeneratingDerivatives.derivativeSum_add_le {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f g : E → F) (N : ℕ) (z : ℝ) (x : E) (hf : ContDiffAt ℝ (↑N) f x) (hg : ContDiffAt ℝ (↑N) g x) (hz : 0 ≤ z) : derivativeSum (f + g) N z x ≤ derivativeSum f N z x + derivativeSum g N z x

theorem EulerGevreyGeneratingDerivatives.norm_iteratedFDeriv_id_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (n : ℕ) (hn : 0 < n) (x : E) : ‖iteratedFDeriv ℝ n id x‖ ≤ if n = 1 then 1 else 0

theorem EulerGevreyGeneratingDerivatives.derivativeSum_id_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (N : ℕ) (z : ℝ) (x : E) (hz : 0 ≤ z) : derivativeSum id N z x ≤ z

theorem EulerGevreyGeneratingDerivatives.derivativeSum_id_add_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : E → E) (N : ℕ) (z : ℝ) (x : E) (hf : ContDiffAt ℝ (↑N) f x) (hz : 0 ≤ z) : derivativeSum (id + f) N z x ≤ z + derivativeSum f N z x

theorem EulerGevreyGeneratingDerivatives.derivativeSum_comp_le {E : Type u_1} {F : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] (f : E → F) (g : F → G) (N : ℕ) (z B R : ℝ) (x : E) (hz : 0 ≤ z) (hB : 0 ≤ B) (hR : 0 ≤ R) (hf : ContDiffAt ℝ (↑N) f x) (hg : ContDiffAt ℝ (↑N) g (f x)) (hgj : ∀ j ∈ Finset.Icc 1 N, ‖iteratedFDeriv ℝ j g (f x)‖ ≤ B * R ^ j * ↑j.factorial ^ 2) (hsmall : R * derivativeSum f N z x < 1) : derivativeSum (g ∘ f) N z x ≤ B * (R * derivativeSum f N z x) / (1 - R * derivativeSum f N z x)

theorem EulerGevreyGeneratingDerivatives.rational_fraction_mono (B x y : ℝ) (hB : 0 ≤ B) (hxy : x ≤ y) (hy : y < 1) : B * x / (1 - x) ≤ B * y / (1 - y)

theorem EulerGevreyGeneratingDerivatives.derivativeSum_comp_id_add_le {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : E → E) (g : E → F) (N : ℕ) (z B R : ℝ) (x : E) (hz : 0 ≤ z) (hB : 0 ≤ B) (hR : 0 ≤ R) (hf : ContDiffAt ℝ (↑N) f x) (hg : ContDiffAt ℝ (↑N) g (x + f x)) (hgj : ∀ j ∈ Finset.Icc 1 N, ‖iteratedFDeriv ℝ j g (x + f x)‖ ≤ B * R ^ j * ↑j.factorial ^ 2) (hsmall : R * (z + derivativeSum f N z x) < 1) : derivativeSum (g ∘ (id + f)) N z x ≤ EulerGevreyFlowBootstrap.rationalRate B R z (derivativeSum f N z x)

The identity part of a flow costs exactly z in its generating sum.