Local Taylor estimates for the four-dimensional Green kernel

The derivative formulas in GreenRemainder are stated at the origin of a coordinate line. The reduction in paper (4.9), however, needs derivatives at every point of a short segment. This file first transports those formulas to an arbitrary parameter on a coordinate line and then proves a one-dimensional quadratic Taylor estimate from the Hessian bound.

The hypotheses of the Green-kernel theorem are geometric: the whole coordinate segment must stay in the open principal cube and a positive distance from the singularity. No Taylor estimate is assumed.

A scalar Taylor estimate

theorem Anderson4D.abs_sub_sub_deriv_mul_le_of_abs_secondDeriv_le {f f' f'' : ℝ → ℝ} {a b M : ℝ} (hM : 0 ≤ M) (hf : ∀ t ∈ Set.uIcc a b, HasDerivAt f (f' t) t) (hf' : ∀ t ∈ Set.uIcc a b, HasDerivAt f' (f'' t) t) (hbound : ∀ t ∈ Set.uIcc a b, |f'' t| ≤ M) : |f b - f a - f' a * (b - a)| ≤ M * |b - a| ^ 2

A scalar function whose second derivative is bounded on the unordered interval between a and b has a quadratic first-order Taylor remainder.

The constant 1 (rather than the sharp 1/2) is convenient for the paper's ≲ estimates and follows directly from two applications of the mean-value inequality.

theorem Anderson4D.abs_sub_le_of_continuousOn_of_abs_deriv_le {f f' : ℝ → ℝ} {a b C : ℝ} (hab : a < b) (hfcont : ContinuousOn f (Set.Icc a b)) (hf : ∀ t ∈ Set.Ioo a b, HasDerivAt f (f' t) t) (hbound : ∀ t ∈ Set.Ioo a b, |f' t| ≤ C) (x : ℝ) : x ∈ Set.Icc a b → ∀ y ∈ Set.Icc a b, |f x - f y| ≤ C * |x - y|

The classical closed-interval Lipschitz estimate, stated with derivatives only on the open interval.

theorem Anderson4D.abs_sub_sub_deriv_mul_le_of_continuousOn {f f' f'' : ℝ → ℝ} {a b M : ℝ} (hab : a < b) (hM : 0 ≤ M) (hfcont : ContinuousOn f (Set.Icc a b)) (hf'cont : ContinuousOn f' (Set.Icc a b)) (hf : ∀ t ∈ Set.Ioo a b, HasDerivAt f (f' t) t) (hf' : ∀ t ∈ Set.Ioo a b, HasDerivAt f' (f'' t) t) (hbound : ∀ t ∈ Set.Ioo a b, |f'' t| ≤ M) : |f b - f a - f' a * (b - a)| ≤ M * (b - a) ^ 2

Closed-interval variant of the scalar Taylor estimate. Derivatives are required only in the open interval; continuity of f and f' identifies the one-sided derivatives at the endpoints. This is the form needed when a Green coordinate path ends on a fundamental-cell face.

theorem Anderson4D.abs_sub_sub_deriv_mul_le_of_continuousOn_rev {f f' f'' : ℝ → ℝ} {a b M : ℝ} (hab : a < b) (hM : 0 ≤ M) (hfcont : ContinuousOn f (Set.Icc a b)) (hf'cont : ContinuousOn f' (Set.Icc a b)) (hf : ∀ t ∈ Set.Ioo a b, HasDerivAt f (f' t) t) (hf' : ∀ t ∈ Set.Ioo a b, HasDerivAt f' (f'' t) t) (hbound : ∀ t ∈ Set.Ioo a b, |f'' t| ≤ M) : |f a - f b - f' b * (a - b)| ≤ 2 * M * (b - a) ^ 2

Reverse-orientation form of the closed-interval Taylor estimate. The factor 2 pays for moving the linearization point from the left endpoint to the right endpoint.

Coordinate-line transport

theorem Anderson4D.coordLine_add_taylor (x : R4) (i : Fin dim) (s t : ℝ) : coordLine (coordLine x i s) i t = coordLine x i (s + t)

theorem Anderson4D.hasDerivAt_greenLocalLift_coord_at {x : R4} (i : Fin dim) {t : ℝ} (hopen : InOpenPrincipalCube (coordLine x i t)) (hne : euclideanDistSq (coordLine x i t) ≠ 0) : HasDerivAt (fun (s : ℝ) => greenLocalLift (coordLine x i s)) (greenLocalGrad (coordLine x i t) i) t

theorem Anderson4D.hasDerivAt_greenLocalGrad_coord_at {x : R4} (i j : Fin dim) {t : ℝ} (hopen : InOpenPrincipalCube (coordLine x j t)) (hne : euclideanDistSq (coordLine x j t) ≠ 0) : HasDerivAt (fun (s : ℝ) => greenLocalGrad (coordLine x j s) i) (greenLocalHess (coordLine x j t) i j) t

Green-kernel Taylor estimate on one coordinate segment

theorem Anderson4D.greenLocalLift_coord_taylor {x : R4} (i : Fin dim) {s M : ℝ} (hM : 0 ≤ M) (hopen : ∀ t ∈ Set.uIcc 0 s, InOpenPrincipalCube (coordLine x i t)) (hne : ∀ t ∈ Set.uIcc 0 s, euclideanDistSq (coordLine x i t) ≠ 0) (hhess : ∀ t ∈ Set.uIcc 0 s, |greenLocalHess (coordLine x i t) i i| ≤ M) : |greenLocalLift (coordLine x i s) - greenLocalLift x - greenLocalGrad x i * s| ≤ M * |s| ^ 2

Coordinate-line Taylor estimate with an explicit Hessian majorant.

theorem Anderson4D.greenLocalHessSingularBound_nonneg : 0 ≤ greenLocalHessSingularBound

theorem Anderson4D.greenLocalLift_coord_taylor_of_radius {x : R4} (i : Fin dim) {s r : ℝ} (hr : 0 < r) (hopen : ∀ t ∈ Set.uIcc 0 s, InOpenPrincipalCube (coordLine x i t)) (hradius : ∀ t ∈ Set.uIcc 0 s, r ≤ √(euclideanDistSq (coordLine x i t))) : |greenLocalLift (coordLine x i s) - greenLocalLift x - greenLocalGrad x i * s| ≤ greenLocalHessSingularBound * r⁻¹ ^ 4 * |s| ^ 2

The preceding Taylor estimate with its Hessian bound discharged from the explicit |x|⁻⁴ estimate. The radius hypothesis says that the whole coordinate segment stays at Euclidean distance at least r from the singularity.

The four-coordinate rectangular path

def Anderson4D.coordinateCorner (a b : R4) (k : Fin (dim + 1)) : R4

The corner obtained by replacing the first k coordinates of a by the corresponding coordinates of b. The five values k = 0, ..., 4 form the rectangular path used below.

Equations

• Anderson4D.coordinateCorner a b k i = if ↑i < ↑k then b i else a i

@[simp]

theorem Anderson4D.coordinateCorner_zero (a b : R4) : coordinateCorner a b 0 = a

@[simp]

theorem Anderson4D.coordinateCorner_last (a b : R4) : coordinateCorner a b ⟨dim, ⋯⟩ = b

theorem Anderson4D.coordinateCorner_succ (a b : R4) (i : Fin dim) : coordinateCorner a b i.succ = coordLine (coordinateCorner a b i.castSucc) i (b i - a i)

Consecutive corners differ by exactly one coordinate line.

theorem Anderson4D.coordinateCorner_telescope (f : R4 → ℝ) (a b : R4) : f b - f a = ∑ i : Fin dim, (f (coordinateCorner a b i.succ) - f (coordinateCorner a b i.castSucc))

Exact telescoping of a function along the four-coordinate rectangular path.

theorem Anderson4D.coordinateCorner_prefix_telescope (f : R4 → ℝ) (a b : R4) (k : Fin (dim + 1)) : f (coordinateCorner a b k) - f a = ∑ i : Fin dim with ↑i < ↑k, (f (coordinateCorner a b i.succ) - f (coordinateCorner a b i.castSucc))

Prefix form of the telescoping identity.

def Anderson4D.coordinateLinearTerm (df : R4 → Fin dim → ℝ) (a b : R4) : ℝ

The coordinate expression for the linear Taylor term at a.

Equations

• Anderson4D.coordinateLinearTerm df a b = ∑ i : Fin Anderson4D.dim, df a i * (b i - a i)

theorem Anderson4D.coordinateTaylor_decomposition (f : R4 → ℝ) (df : R4 → Fin dim → ℝ) (a b : R4) : f b - f a - coordinateLinearTerm df a b = ∑ i : Fin dim, (f (coordinateCorner a b i.succ) - f (coordinateCorner a b i.castSucc) - df (coordinateCorner a b i.castSucc) i * (b i - a i)) + ∑ i : Fin dim, (df (coordinateCorner a b i.castSucc) i - df a i) * (b i - a i)

Exact decomposition into the four one-coordinate Taylor remainders and the cost of moving the gradient from each intermediate corner back to the initial point.

def Anderson4D.coordinateL1Dist (a b : R4) : ℝ

The ℓ¹ length of the displacement used by the rectangular path.

Equations

• Anderson4D.coordinateL1Dist a b = ∑ i : Fin Anderson4D.dim, |b i - a i|

theorem Anderson4D.coordinateL1Dist_nonneg (a b : R4) : 0 ≤ coordinateL1Dist a b

theorem Anderson4D.coordinateTaylor_bound (f : R4 → ℝ) (df : R4 → Fin dim → ℝ) (a b : R4) {M : ℝ} (hM : 0 ≤ M) (hremainder : ∀ (i : Fin dim), |f (coordinateCorner a b i.succ) - f (coordinateCorner a b i.castSucc) - df (coordinateCorner a b i.castSucc) i * (b i - a i)| ≤ M * |b i - a i| ^ 2) (hgradient : ∀ (i : Fin dim), |df (coordinateCorner a b i.castSucc) i - df a i| ≤ M * coordinateL1Dist a b) : |f b - f a - coordinateLinearTerm df a b| ≤ 2 * M * coordinateL1Dist a b ^ 2

A quantitative rectangular-path Taylor lemma. It separates the two analytic inputs needed later:

• a quadratic remainder on each coordinate edge;
• a Lipschitz estimate comparing the gradient at an intermediate corner to the gradient at the initial point.

For the Green kernel, both inputs follow from its Hessian estimate.

Moving the Green gradient along the rectangular path

theorem Anderson4D.greenLocalGrad_coord_lipschitz_of_radius {x : R4} (i j : Fin dim) {s r : ℝ} (hr : 0 < r) (hopen : ∀ t ∈ Set.uIcc 0 s, InOpenPrincipalCube (coordLine x j t)) (hradius : ∀ t ∈ Set.uIcc 0 s, r ≤ √(euclideanDistSq (coordLine x j t))) : |greenLocalGrad (coordLine x j s) i - greenLocalGrad x i| ≤ greenLocalHessSingularBound * r⁻¹ ^ 4 * |s|

A coordinate entry of the Green gradient is Lipschitz along one coordinate segment, with the Lipschitz constant supplied by the singular Hessian estimate.

theorem Anderson4D.greenLocalGrad_coordinateCorner_edge (a b : R4) (i j : Fin dim) {r : ℝ} (hr : 0 < r) (hopen : ∀ t ∈ Set.uIcc 0 (b j - a j), InOpenPrincipalCube (coordLine (coordinateCorner a b j.castSucc) j t)) (hradius : ∀ t ∈ Set.uIcc 0 (b j - a j), r ≤ √(euclideanDistSq (coordLine (coordinateCorner a b j.castSucc) j t))) : |greenLocalGrad (coordinateCorner a b j.succ) i - greenLocalGrad (coordinateCorner a b j.castSucc) i| ≤ greenLocalHessSingularBound * r⁻¹ ^ 4 * |b j - a j|

One edge of the rectangular path, in the form used to compare intermediate gradients.

theorem Anderson4D.greenLocalGrad_coordinateCorner_le (a b : R4) (i : Fin dim) {r : ℝ} (hr : 0 < r) (hopen : ∀ (j : Fin dim), ∀ t ∈ Set.uIcc 0 (b j - a j), InOpenPrincipalCube (coordLine (coordinateCorner a b j.castSucc) j t)) (hradius : ∀ (j : Fin dim), ∀ t ∈ Set.uIcc 0 (b j - a j), r ≤ √(euclideanDistSq (coordLine (coordinateCorner a b j.castSucc) j t))) : |greenLocalGrad (coordinateCorner a b i.castSucc) i - greenLocalGrad a i| ≤ greenLocalHessSingularBound * r⁻¹ ^ 4 * coordinateL1Dist a b

Every intermediate rectangular-path gradient differs from the initial gradient by at most the Hessian constant times the full ℓ¹ path length. The proof uses the exact prefix telescope and then enlarges the prefix to all four nonnegative edge contributions.

theorem Anderson4D.greenLocalLift_rectangular_taylor_of_radius (a b : R4) {r : ℝ} (hr : 0 < r) (hopen : ∀ (j : Fin dim), ∀ t ∈ Set.uIcc 0 (b j - a j), InOpenPrincipalCube (coordLine (coordinateCorner a b j.castSucc) j t)) (hradius : ∀ (j : Fin dim), ∀ t ∈ Set.uIcc 0 (b j - a j), r ≤ √(euclideanDistSq (coordLine (coordinateCorner a b j.castSucc) j t))) : |greenLocalLift b - greenLocalLift a - coordinateLinearTerm greenLocalGrad a b| ≤ 2 * (greenLocalHessSingularBound * r⁻¹ ^ 4) * coordinateL1Dist a b ^ 2

Four-dimensional local Taylor estimate for the Green kernel. All analytic hypotheses are now geometric: every edge of the rectangular path stays in the open principal cube and at distance at least r from the singularity.

Torus-valued endpoints

@[simp]

theorem Anderson4D.greenLocalPoint_torusLift (z : T4) : greenLocalPoint (torusLift z) = z

@[simp]

theorem Anderson4D.greenLocalLift_torusLift (z : T4) : greenLocalLift (torusLift z) = greenFn z

theorem Anderson4D.greenFn_rectangular_taylor_of_safe_lifts (u v : T4) {r : ℝ} (hr : 0 < r) (hopen : ∀ (j : Fin dim), ∀ t ∈ Set.uIcc 0 (torusLift v j - torusLift u j), InOpenPrincipalCube (coordLine (coordinateCorner (torusLift u) (torusLift v) j.castSucc) j t)) (hradius : ∀ (j : Fin dim), ∀ t ∈ Set.uIcc 0 (torusLift v j - torusLift u j), r ≤ √(euclideanDistSq (coordLine (coordinateCorner (torusLift u) (torusLift v) j.castSucc) j t))) : |greenFn v - greenFn u - coordinateLinearTerm greenLocalGrad (torusLift u) (torusLift v)| ≤ 2 * (greenLocalHessSingularBound * r⁻¹ ^ 4) * coordinateL1Dist (torusLift u) (torusLift v) ^ 2

Torus form of the rectangular Taylor estimate. The hypotheses expose the exact chart-safety facts which a later geometric region decomposition must establish; the conclusion is already about greenFn, not an auxiliary Euclidean kernel.

Periodicity of the differentiated lattice sum

noncomputable def Anderson4D.fullLatticeGreenValue (x : R4) : ℝ

The full scalar lattice sum. This representation is used only to control limits at the boundary of the half-open fundamental cell.

Equations

• Anderson4D.fullLatticeGreenValue x = ∑' (k : Anderson4D.Z4), Anderson4D.latticeBesselTerm x k

noncomputable def Anderson4D.fullLatticeGreenGrad (x : R4) (i : Fin dim) : ℝ

The full first-derivative lattice sum. Unlike the zero-plus-remainder presentation of greenLocalGrad, this form makes periodic reindexing transparent.

Equations

• Anderson4D.fullLatticeGreenGrad x i = ∑' (k : Anderson4D.Z4), Anderson4D.latticeBesselGrad x k i

noncomputable def Anderson4D.fullLatticeGreenHess (x : R4) (i j : Fin dim) : ℝ

The full second-derivative lattice sum.

Equations

• Anderson4D.fullLatticeGreenHess x i j = ∑' (k : Anderson4D.Z4), Anderson4D.latticeBesselHess x k i j

theorem Anderson4D.fullLatticeGreenValue_eq_of_mem_Ico {x : R4} (hx : ∀ (i : Fin dim), x i ∈ Set.Ico (-Real.pi) Real.pi) (hne : euclideanDistSq x ≠ 0) : fullLatticeGreenValue x = greenLocalLift x

theorem Anderson4D.fullLatticeGreenGrad_eq {x : R4} (hx : InClosedPrincipalCube x) (i : Fin dim) : fullLatticeGreenGrad x i = greenLocalGrad x i

theorem Anderson4D.fullLatticeGreenHess_eq {x : R4} (hx : InClosedPrincipalCube x) (i j : Fin dim) : fullLatticeGreenHess x i j = greenLocalHess x i j

noncomputable def Anderson4D.realPeriodShift (m : Z4) : R4

Real representative of an integer period shift.

Equations

• Anderson4D.realPeriodShift m i = 2 * Real.pi * ↑(m i)

theorem Anderson4D.fullLatticeGreenGrad_add_period (x : R4) (m : Z4) (i : Fin dim) : fullLatticeGreenGrad (x + realPeriodShift m) i = fullLatticeGreenGrad x i

theorem Anderson4D.fullLatticeGreenHess_add_period (x : R4) (m : Z4) (i j : Fin dim) : fullLatticeGreenHess (x + realPeriodShift m) i j = fullLatticeGreenHess x i j

theorem Anderson4D.fullLatticeGreenValue_add_period (x : R4) (m : Z4) : fullLatticeGreenValue (x + realPeriodShift m) = fullLatticeGreenValue x

theorem Anderson4D.greenLocalLift_add_period (x : R4) (m : Z4) : greenLocalLift (x + realPeriodShift m) = greenLocalLift x

The pulled-back Green value is globally periodic, directly from the quotient definition.

theorem Anderson4D.greenLocalPoint_add_period (x : R4) (m : Z4) : greenLocalPoint (x + realPeriodShift m) = greenLocalPoint x

theorem Anderson4D.greenLocalGrad_add_period_of_closed {x : R4} (m : Z4) (hx : InClosedPrincipalCube x) (hshift : InClosedPrincipalCube (x + realPeriodShift m)) (i : Fin dim) : greenLocalGrad (x + realPeriodShift m) i = greenLocalGrad x i

A closed fundamental cell differs from the half-open canonical cell only at coordinates equal to π. The following explicit replacement is useful for transporting identities to those boundary faces.

noncomputable def Anderson4D.halfOpenRepresentative (x : R4) : R4

Equations

• Anderson4D.halfOpenRepresentative x i = if x i = Real.pi then -Real.pi else x i

noncomputable def Anderson4D.halfOpenPeriodShift (x : R4) : Z4

Equations

• Anderson4D.halfOpenPeriodShift x i = if x i = Real.pi then -1 else 0

theorem Anderson4D.add_halfOpenPeriodShift (x : R4) : x + realPeriodShift (halfOpenPeriodShift x) = halfOpenRepresentative x

theorem Anderson4D.halfOpenRepresentative_mem_Ico {x : R4} (hx : InClosedPrincipalCube x) (i : Fin dim) : halfOpenRepresentative x i ∈ Set.Ico (-Real.pi) Real.pi

theorem Anderson4D.euclideanDistSq_halfOpenRepresentative (x : R4) : euclideanDistSq (halfOpenRepresentative x) = euclideanDistSq x

theorem Anderson4D.torusDistSq_greenLocalPoint_of_closed {x : R4} (hx : InClosedPrincipalCube x) : torusDistSq (greenLocalPoint x) = euclideanDistSq x

theorem Anderson4D.torusLift_greenLocalPoint_of_closed {x : R4} (hx : InClosedPrincipalCube x) : torusLift (greenLocalPoint x) = halfOpenRepresentative x

theorem Anderson4D.greenLocalGrad_halfOpenRepresentative {x : R4} (hx : InClosedPrincipalCube x) (i : Fin dim) : greenLocalGrad (halfOpenRepresentative x) i = greenLocalGrad x i

theorem Anderson4D.greenLocalLift_halfOpenRepresentative (x : R4) : greenLocalLift (halfOpenRepresentative x) = greenLocalLift x

theorem Anderson4D.fullLatticeGreenValue_eq {x : R4} (hx : InClosedPrincipalCube x) (hne : euclideanDistSq x ≠ 0) : fullLatticeGreenValue x = greenLocalLift x

The full scalar lattice sum agrees with the pulled-back Green kernel also on the closed faces of the principal cube.

theorem Anderson4D.greenLocalGrad_lower_upper_boundary {x : R4} (hx : InClosedPrincipalCube x) (j i : Fin dim) (hxj : x j = -Real.pi) : greenLocalGrad (coordLine x j (2 * Real.pi)) i = greenLocalGrad x i

The two boundary representatives -π and π give the same Green gradient. This is the gluing identity needed when a short coordinate segment wraps around the fundamental cell.

theorem Anderson4D.greenLocalHess_lower_upper_boundary {x : R4} (hx : InClosedPrincipalCube x) (j i k : Fin dim) (hxj : x j = -Real.pi) : greenLocalHess (coordLine x j (2 * Real.pi)) i k = greenLocalHess x i k

One-dimensional continuity up to the cell boundary

The Taylor path may meet a face of the closed principal cube. The following lemmas give the missing endpoint continuity directly from the uniformly summable lattice series. They deliberately concern a single coordinate line; this is exactly what is needed to glue the finitely many pieces of a wrapped rectangular path.

theorem Anderson4D.hasDerivAt_greenLocalLift_coord_closed {x : R4} (hx : InClosedPrincipalCube x) (hne : euclideanDistSq x ≠ 0) (j : Fin dim) (hxj : |x j| < Real.pi) : HasDerivAt (fun (s : ℝ) => greenLocalLift (coordLine x j s)) (greenLocalGrad x j) 0

Coordinate derivative of the pulled-back Green kernel at a point of the closed cell whose moving coordinate is not on a face. Other coordinates are allowed to lie on faces.

theorem Anderson4D.hasDerivAt_greenLocalGrad_coord_closed {x : R4} (hx : InClosedPrincipalCube x) (hne : euclideanDistSq x ≠ 0) (i j : Fin dim) (hxj : |x j| < Real.pi) : HasDerivAt (fun (s : ℝ) => greenLocalGrad (coordLine x j s) i) (greenLocalHess x i j) 0

theorem Anderson4D.hasDerivAt_greenLocalLift_coord_closed_at {x : R4} (j : Fin dim) {t : ℝ} (hclosed : InClosedPrincipalCube (coordLine x j t)) (hne : euclideanDistSq (coordLine x j t) ≠ 0) (hcoord : |coordLine x j t j| < Real.pi) : HasDerivAt (fun (s : ℝ) => greenLocalLift (coordLine x j s)) (greenLocalGrad (coordLine x j t) j) t

theorem Anderson4D.hasDerivAt_greenLocalGrad_coord_closed_at {x : R4} (i j : Fin dim) {t : ℝ} (hclosed : InClosedPrincipalCube (coordLine x j t)) (hne : euclideanDistSq (coordLine x j t) ≠ 0) (hcoord : |coordLine x j t j| < Real.pi) : HasDerivAt (fun (s : ℝ) => greenLocalGrad (coordLine x j s) i) (greenLocalHess (coordLine x j t) i j) t

theorem Anderson4D.continuousOn_nonzeroLatticeRemainder_coord {x : R4} (j : Fin dim) {s : Set ℝ} (hclosed : ∀ t ∈ s, InClosedPrincipalCube (coordLine x j t)) : ContinuousOn (fun (t : ℝ) => nonzeroLatticeRemainder (coordLine x j t)) s

theorem Anderson4D.continuousOn_nonzeroLatticeRemainderGrad_coord {x : R4} (i j : Fin dim) {s : Set ℝ} (hclosed : ∀ t ∈ s, InClosedPrincipalCube (coordLine x j t)) : ContinuousOn (fun (t : ℝ) => nonzeroLatticeRemainderGrad (coordLine x j t) i) s

theorem Anderson4D.continuousOn_greenLocalLift_coord_closed {x : R4} (j : Fin dim) {s : Set ℝ} (hclosed : ∀ t ∈ s, InClosedPrincipalCube (coordLine x j t)) (hne : ∀ t ∈ s, euclideanDistSq (coordLine x j t) ≠ 0) : ContinuousOn (fun (t : ℝ) => greenLocalLift (coordLine x j t)) s

theorem Anderson4D.continuousOn_greenLocalGrad_coord_closed {x : R4} (i j : Fin dim) {s : Set ℝ} (hclosed : ∀ t ∈ s, InClosedPrincipalCube (coordLine x j t)) (hne : ∀ t ∈ s, euclideanDistSq (coordLine x j t) ≠ 0) : ContinuousOn (fun (t : ℝ) => greenLocalGrad (coordLine x j t) i) s

theorem Anderson4D.greenLocalLift_coord_taylor_closed_interval_of_radius {x : R4} (j : Fin dim) {a b r : ℝ} (hab : a < b) (hr : 0 < r) (hclosed : ∀ t ∈ Set.Icc a b, InClosedPrincipalCube (coordLine x j t)) (hcoord : ∀ t ∈ Set.Ioo a b, |coordLine x j t j| < Real.pi) (hradius : ∀ t ∈ Set.Icc a b, r ≤ √(euclideanDistSq (coordLine x j t))) : |greenLocalLift (coordLine x j b) - greenLocalLift (coordLine x j a) - greenLocalGrad (coordLine x j a) j * (b - a)| ≤ greenLocalHessSingularBound * r⁻¹ ^ 4 * (b - a) ^ 2

Taylor estimate on a coordinate interval contained in the closed principal cell. The endpoints may lie on cell faces; only interior points must have their moving coordinate in the open cell.

theorem Anderson4D.greenLocalGrad_coord_lipschitz_closed_interval_of_radius {x : R4} (i j : Fin dim) {a b r : ℝ} (hab : a < b) (hr : 0 < r) (hclosed : ∀ t ∈ Set.Icc a b, InClosedPrincipalCube (coordLine x j t)) (hcoord : ∀ t ∈ Set.Ioo a b, |coordLine x j t j| < Real.pi) (hradius : ∀ t ∈ Set.Icc a b, r ≤ √(euclideanDistSq (coordLine x j t))) : |greenLocalGrad (coordLine x j b) i - greenLocalGrad (coordLine x j a) i| ≤ greenLocalHessSingularBound * r⁻¹ ^ 4 * (b - a)

Gradient Lipschitz estimate on the same closed coordinate interval.

theorem Anderson4D.greenLocalLift_coord_taylor_closed_interval_rev_of_radius {x : R4} (j : Fin dim) {a b r : ℝ} (hab : a < b) (hr : 0 < r) (hclosed : ∀ t ∈ Set.Icc a b, InClosedPrincipalCube (coordLine x j t)) (hcoord : ∀ t ∈ Set.Ioo a b, |coordLine x j t j| < Real.pi) (hradius : ∀ t ∈ Set.Icc a b, r ≤ √(euclideanDistSq (coordLine x j t))) : |greenLocalLift (coordLine x j a) - greenLocalLift (coordLine x j b) - greenLocalGrad (coordLine x j b) j * (a - b)| ≤ 2 * (greenLocalHessSingularBound * r⁻¹ ^ 4) * (b - a) ^ 2

Reverse traversal of a closed coordinate interval, linearized at the right endpoint.