Newton--Taylor formulas from Carlson's Dirichlet averages

This file develops Carlson's Section 5.5. The unweighted Dirichlet average is isolated first, and divided differences are defined from averages of iterated derivatives. Canonical finite index types are used for lists of interpolation nodes; permutation invariance can subsequently remove any dependence on their chosen ordering.

Carlson's Lemma 5.5-1 follows from the fundamental theorem of calculus on the last free-coordinate slices of a simplex. A second slicing and dilation formula proves the repeated-integral identity. Both arguments allow coincident nodes.

References

• [Carl77] B. C. Carlson, Special Functions of Applied Mathematics, Section 5.5, Academic Press, 1977.

noncomputable def DirichletTransform.carlsonUnweightedAverage {ι : Type u_1} [Fintype ι] (z : ι → ℂ) (f : ℂ → ℂ) : ℂ

Carlson's unweighted Dirichlet average, obtained by setting every Dirichlet parameter equal to one.

Equations

• DirichletTransform.carlsonUnweightedAverage z f = DirichletTransform.realCarlsonDirichletAverage (fun (x : ι) => 1) z f

theorem DirichletTransform.one_mem_mvRealBetaDomain {ι : Type u_1} : (fun (x : ι) => 1) ∈ ProbabilityTheory.mvRealBetaDomain

The unweighted Dirichlet parameters belong to the positive real parameter domain.

theorem DirichletTransform.carlsonUnweightedAverage_const {ι : Type u_1} [Fintype ι] [Nonempty ι] (f : ℂ → ℂ) (w : ℂ) : carlsonUnweightedAverage (fun (x : ι) => w) f = f w

Averaging at a constant vector of nodes is evaluation at that node.

theorem DirichletTransform.carlsonUnweightedAverage_perm {ι : Type u_1} [Fintype ι] (z : ι → ℂ) (f : ℂ → ℂ) (σ : Equiv.Perm ι) : carlsonUnweightedAverage (z ∘ ⇑σ) f = carlsonUnweightedAverage z f

Permuting the nodes does not change the unweighted Carlson average.

def DirichletTransform.prependNewtonNode {n : ℕ} (x : ℂ) (z : Fin n → ℂ) : Fin (n + 1) → ℂ

The node vector obtained by placing x before a vector of n nodes.

Equations

• DirichletTransform.prependNewtonNode x z = Fin.cons x z

def DirichletTransform.prependTwoNewtonNodes {n : ℕ} (x y : ℂ) (z : Fin n → ℂ) : Fin (n + 2) → ℂ

The node vector obtained by placing x and y before a vector of n nodes.

Equations

• DirichletTransform.prependTwoNewtonNodes x y z = Fin.cons x (Fin.cons y z)

noncomputable def DirichletTransform.carlsonDividedDifference (n : ℕ) (f : ℂ → ℂ) (z : Fin (n + 1) → ℂ) : ℂ

A divided difference of order n, expressed as Carlson's unweighted average of the nth derivative divided by n!; this is formula (5.5-6).

Equations

• DirichletTransform.carlsonDividedDifference n f z = DirichletTransform.carlsonUnweightedAverage z (iteratedDeriv n f) / ↑n.factorial

theorem DirichletTransform.carlsonUnweightedAverage_eq_factorial_integral {n : ℕ} (z : Fin (n + 1) → ℂ) (f : ℂ → ℂ) : carlsonUnweightedAverage z f = ↑n.factorial * ∫ (u : Fin (n + 1) → ℝ) in Convexity.StdSimplex.coordinateSet ℝ (Fin (n + 1)), f (carlsonAffineForm z u) ∂MeasureTheory.Measure.stdSimplexMeasure

Unweighted probability normalization in finite coordinates.

theorem DirichletTransform.carlsonDividedDifference_eq_integral {n : ℕ} (z : Fin (n + 1) → ℂ) (f : ℂ → ℂ) : carlsonDividedDifference n f z = ∫ (v : Fin n → ℝ) in posSimplexFin n 1, iteratedDeriv n f (carlsonAffineForm z (MeasureTheory.finSimplexPoint v))

The factorial in the divided difference cancels the probability normalization.

theorem DirichletTransform.carlson_simplex_integral_sub {n : ℕ} {Ω : Set ℂ} (hΩconv : Convex ℝ Ω) {f : ℂ → ℂ} (hf : AnalyticOnNhd ℂ f Ω) (z : Fin n → ℂ) (hz : Set.range z ⊆ Ω) {x y : ℂ} (hx : x ∈ Ω) (hy : y ∈ Ω) : (∫ (v : Fin n → ℝ) in posSimplexFin n 1, f (carlsonAffineForm (Fin.snoc z x) (MeasureTheory.finSimplexPoint v))) - ∫ (v : Fin n → ℝ) in posSimplexFin n 1, f (carlsonAffineForm (Fin.snoc z y) (MeasureTheory.finSimplexPoint v)) = (x - y) * ∫ (v : Fin (n + 1) → ℝ) in posSimplexFin (n + 1) 1, deriv f (carlsonAffineForm (Fin.snoc (Fin.snoc z x) y) (MeasureTheory.finSimplexPoint v))

The simplex fundamental theorem of calculus for a holomorphic kernel.

theorem DirichletTransform.carlsonDividedDifference_perm (n : ℕ) (f : ℂ → ℂ) (z : Fin (n + 1) → ℂ) (σ : Equiv.Perm (Fin (n + 1))) : carlsonDividedDifference n f (z ∘ ⇑σ) = carlsonDividedDifference n f z

Divided differences are invariant under permutations of their nodes.

theorem DirichletTransform.carlsonDividedDifference_snoc_snoc_comm (n : ℕ) (f : ℂ → ℂ) (z : Fin n → ℂ) (x y : ℂ) : carlsonDividedDifference (n + 1) f (Fin.snoc (Fin.snoc z x) y) = carlsonDividedDifference (n + 1) f (Fin.snoc (Fin.snoc z y) x)

Exchanging the final two nodes does not change a divided difference.

@[simp]

theorem DirichletTransform.carlsonDividedDifference_zero (f : ℂ → ℂ) (z : Fin 1 → ℂ) : carlsonDividedDifference 0 f z = f (z 0)

A divided difference of order zero is evaluation at its unique node.

theorem DirichletTransform.carlsonDividedDifference_const (n : ℕ) (f : ℂ → ℂ) (w : ℂ) : (carlsonDividedDifference n f fun (x : Fin (n + 1)) => w) = iteratedDeriv n f w / ↑n.factorial

If all nodes coincide, Carlson's divided difference is the corresponding Taylor coefficient.

def DirichletTransform.newtonBasis {n : ℕ} (z : Fin n → ℂ) (x : ℂ) : ℂ

The Newton basis polynomial associated to a finite vector of preceding nodes.

Equations

• DirichletTransform.newtonBasis z x = ∏ i : Fin n, (x - z i)

@[simp]

theorem DirichletTransform.newtonBasis_zero (z : Fin 0 → ℂ) (x : ℂ) : newtonBasis z x = 1

The empty Newton basis is one.

@[simp]

theorem DirichletTransform.newtonBasis_prepend {n : ℕ} (z : Fin n → ℂ) (a x : ℂ) : newtonBasis (prependNewtonNode a z) x = (x - a) * newtonBasis z x

Prepending a node adds the corresponding linear factor to the Newton basis.

theorem DirichletTransform.newtonBasis_snoc {n : ℕ} (z : Fin n → ℂ) (a x : ℂ) : newtonBasis (Fin.snoc z a) x = newtonBasis z x * (x - a)

Appending a node adds its linear factor to the Newton basis.

def DirichletTransform.newtonPrecedingNodes {p : ℕ} (z : Fin p → ℂ) (n : Fin p) : Fin ↑n → ℂ

The nodes preceding the coefficient indexed by n in a finite Newton expansion.

Equations

• DirichletTransform.newtonPrecedingNodes z n i = z ⟨↑i, ⋯⟩

def DirichletTransform.newtonPrefix {p : ℕ} (z : Fin p → ℂ) (n : Fin p) : Fin (↑n + 1) → ℂ

The nodes through the coefficient indexed by n in a finite Newton expansion.

Equations

• DirichletTransform.newtonPrefix z n i = z ⟨↑i, ⋯⟩

@[simp]

theorem DirichletTransform.newtonPrecedingNodes_init_castSucc {p : ℕ} (z : Fin (p + 1) → ℂ) (n : Fin p) : newtonPrecedingNodes z n.castSucc = newtonPrecedingNodes (Fin.init z) n

@[simp]

theorem DirichletTransform.newtonPrefix_init_castSucc {p : ℕ} (z : Fin (p + 1) → ℂ) (n : Fin p) : newtonPrefix z n.castSucc = newtonPrefix (Fin.init z) n

@[simp]

theorem DirichletTransform.newtonPrecedingNodes_last {p : ℕ} (z : Fin (p + 1) → ℂ) : newtonPrecedingNodes z (Fin.last p) = Fin.init z

@[simp]

theorem DirichletTransform.newtonPrefix_last {p : ℕ} (z : Fin (p + 1) → ℂ) : newtonPrefix z (Fin.last p) = z

theorem DirichletTransform.carlsonDividedDifference_sub {n : ℕ} {Ω : Set ℂ} (hΩconv : Convex ℝ Ω) {f : ℂ → ℂ} (hf : AnalyticOnNhd ℂ f Ω) (z : Fin n → ℂ) (hz : Set.range z ⊆ Ω) {x y : ℂ} (hx : x ∈ Ω) (hy : y ∈ Ω) : carlsonDividedDifference n f (Fin.snoc z x) - carlsonDividedDifference n f (Fin.snoc z y) = (x - y) * carlsonDividedDifference (n + 1) f (Fin.snoc (Fin.snoc z x) y)

Carlson 5.5-1. Divided differences defined by unweighted Dirichlet averages satisfy the usual first-order recurrence, including at coincident nodes.

theorem DirichletTransform.newtonTaylor_sum_add_remainder {p : ℕ} {Ω : Set ℂ} (hΩconv : Convex ℝ Ω) {f : ℂ → ℂ} (hf : AnalyticOnNhd ℂ f Ω) (z : Fin p → ℂ) (hz : Set.range z ⊆ Ω) {x : ℂ} (hx : x ∈ Ω) : f x = ∑ n : Fin p, carlsonDividedDifference (↑n) f (newtonPrefix z n) * newtonBasis (newtonPrecedingNodes z n) x + carlsonDividedDifference p f (Fin.snoc z x) * newtonBasis z x

Carlson 5.5-2. The finite Newton expansion with its Dirichlet-average remainder.

theorem DirichletTransform.taylor_sum_add_carlsonRemainder {Ω : Set ℂ} (hΩconv : Convex ℝ Ω) {f : ℂ → ℂ} (hf : AnalyticOnNhd ℂ f Ω) {a x : ℂ} (ha : a ∈ Ω) (hx : x ∈ Ω) (p : ℕ) : f x = ∑ n : Fin p, iteratedDeriv (↑n) f a / ↑(↑n).factorial * (x - a) ^ ↑n + carlsonDividedDifference p f (Fin.snoc (fun (x : Fin p) => a) x) * (x - a) ^ p

Taylor's formula with Carlson's unweighted-average remainder, obtained from the Newton--Taylor formula by coalescing all interpolation nodes.

Repeated integrals

noncomputable def DirichletTransform.carlsonSegmentIntegral (a x : ℂ) (f : ℂ → ℂ) : ℂ

Integration of a complex-valued function along the oriented segment from a to x.

Equations

• DirichletTransform.carlsonSegmentIntegral a x f = (x - a) * ∫ (t : ℝ) in 0..1, f (a + ↑t * (x - a))

def DirichletTransform.carlsonRepeatedIntegral : ℕ → ℂ → (ℂ → ℂ) → ℂ → ℂ

Carlson's repeated integration operator based at a, defined recursively by segment integration. This is the operator in equations 5.5(9) and 5.5(12).

Equations

• DirichletTransform.carlsonRepeatedIntegral 0 x✝² x✝¹ x✝ = x✝¹ x✝
• DirichletTransform.carlsonRepeatedIntegral n.succ x✝² x✝¹ x✝ = DirichletTransform.carlsonSegmentIntegral x✝² x✝ (DirichletTransform.carlsonRepeatedIntegral n x✝² x✝¹)

@[simp]

theorem DirichletTransform.carlsonRepeatedIntegral_zero (a : ℂ) (f : ℂ → ℂ) (x : ℂ) : carlsonRepeatedIntegral 0 a f x = f x

The zeroth repeated integral is the original function.

@[simp]

theorem DirichletTransform.carlsonRepeatedIntegral_succ (n : ℕ) (a : ℂ) (f : ℂ → ℂ) (x : ℂ) : carlsonRepeatedIntegral (n + 1) a f x = carlsonSegmentIntegral a x (carlsonRepeatedIntegral n a f)

The successor step for Carlson's repeated integration operator.

theorem DirichletTransform.carlsonRepeatedIntegral_eq_unweightedAverage {Ω : Set ℂ} (hΩconv : Convex ℝ Ω) {f : ℂ → ℂ} (hf : AnalyticOnNhd ℂ f Ω) {a x : ℂ} (ha : a ∈ Ω) (hx : x ∈ Ω) (n : ℕ) : carlsonRepeatedIntegral n a f x = (x - a) ^ n / ↑n.factorial * carlsonUnweightedAverage (Fin.snoc (fun (x : Fin n) => a) x) f

Carlson's equation 5.5(10): an n-fold repeated integral is an unweighted Dirichlet average with n nodes coalesced at the base point and one node at the endpoint.