Ported for Lean Pool: imports relocated and code adapted to Lean/Mathlib v4.34.0.

Strictification and jet bridges for the Aleksandrov--Jensen argument (CoordinateQuartic)

Part of the quartic strictification, compact Hessian, and jet transport development used before the contact-set and approximation arguments in SemiconvexJensen. Split from Strictification.lean; see the umbrella module docstring.

theorem ViscositySolns.exists_mem_of_measure_pos_of_measure_compl_property_zero {n : ℕ} {K : Set (Point n)} {P : Point n → Prop} (hKpos : 0 < MeasureTheory.volume K) (hnull : MeasureTheory.volume {x : Point n | ¬P x} = 0) : ∃ x ∈ K, P x

If K has positive Lebesgue measure and the set where P fails has measure zero, then some point of K satisfies P.

theorem ViscositySolns.exists_mem_of_measure_pos_of_measure_inter_compl_property_zero {n : ℕ} {K : Set (Point n)} {P : Point n → Prop} (hKpos : 0 < MeasureTheory.volume K) (hnull : MeasureTheory.volume (K ∩ {x : Point n | ¬P x}) = 0) : ∃ x ∈ K, P x

If K has positive Lebesgue measure and the subset of K where P fails has measure zero, then some point of K satisfies P.

def ViscositySolns.coordinateQuartic {n : ℕ} (x : Point n) : ℝ

The coordinate quartic used in the source proof to make the maximum strict.

In quantified mathematical form, this is x ↦ (∑ i, x_i^2)^2.

Equations

• ViscositySolns.coordinateQuartic x = (x ⬝ᵥ x) ^ 2

@[simp]

theorem ViscositySolns.coordinateQuartic_zero {n : ℕ} : coordinateQuartic 0 = 0

theorem ViscositySolns.continuous_coordinateQuartic {n : ℕ} : Continuous coordinateQuartic

The coordinate quartic is continuous.

theorem ViscositySolns.dotProduct_self_convex_combination {n : ℕ} (x y : Point n) {a b : ℝ} (hab : a + b = 1) : (a • x + b • y) ⬝ᵥ (a • x + b • y) + a * b * (x - y) ⬝ᵥ (x - y) = a * x ⬝ᵥ x + b * y ⬝ᵥ y

The coordinate quadratic identity underlying the quartic estimate.

In quantified mathematical form, if a + b = 1, then

∑ i (a x_i + b y_i)^2 + a b ∑ i (x_i - y_i)^2 = a ∑ i x_i^2 + b ∑ i y_i^2.

theorem ViscositySolns.coordinateQuartic_convex_combination_defect_le_closedBall {n : ℕ} {r : ℝ} (hr : 0 ≤ r) {x y : Point n} (hx : x ∈ Metric.closedBall 0 r) (hy : y ∈ Metric.closedBall 0 r) {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) : a * coordinateQuartic x + b * coordinateQuartic y - coordinateQuartic (a • x + b • y) ≤ (4 * ↑n ^ 2 * r ^ 2 + 2 * ↑n * r ^ 2) * a * b * (x - y) ⬝ᵥ (x - y)

The defect in the coordinate quartic is bounded on a closed ball.

In quantified mathematical form, suppose 0 ≤ r, x ∈ closedBall 0 r, y ∈ closedBall 0 r, a ≥ 0, b ≥ 0, and a + b = 1. Then

`a (∑ i x_i^2)^2 + b (∑ i y_i^2)^2

• (∑ i (a x_i + b y_i)^2)^2`

is at most

(4 n^2 r^2 + 2 n r^2) a b ∑ i (x_i - y_i)^2.

theorem ViscositySolns.coordinateSemiconvexOn_neg_coordinateQuartic_closedBall {n : ℕ} {r : ℝ} (hr : 0 ≤ r) : CoordinateSemiconvexOn (2 * (4 * ↑n ^ 2 * r ^ 2 + 2 * ↑n * r ^ 2)) (Metric.closedBall 0 r) fun (x : Point n) => -coordinateQuartic x

The negative coordinate quartic is coordinate semiconvex on a closed ball.

In quantified mathematical form, if 0 ≤ r, then the function

x ↦ - (∑ i x_i^2)^2

satisfies the coordinate semiconvexity inequality on closedBall 0 r with constant

2 * (4 n^2 r^2 + 2 n r^2).

theorem ViscositySolns.contDiff_coordinateQuartic {n : ℕ} : ContDiff ℝ ⊤ coordinateQuartic

The coordinate quartic is smooth.

def ViscositySolns.coordinateSquareSum {n : ℕ} (x : Point n) : ℝ

The coordinate square-sum x ↦ ∑ i, x_i^2.

Equations

• ViscositySolns.coordinateSquareSum x = ∑ i : Fin n, x i * x i

def ViscositySolns.coordinateSquareSumFDeriv {n : ℕ} (x : Point n) : Point n →L[ℝ] ℝ

The first Fréchet derivative of the coordinate square-sum, written as a continuous linear map.

Equations

• ViscositySolns.coordinateSquareSumFDeriv x = ∑ i : Fin n, (x i • ContinuousLinearMap.proj i + x i • ContinuousLinearMap.proj i)

theorem ViscositySolns.hasFDerivWithinAt_coordinateSquareSum_zero {n : ℕ} : HasFDerivWithinAt coordinateSquareSum 0 Set.univ 0

At the origin, the coordinate square-sum has zero first Fréchet derivative.

@[simp]

theorem ViscositySolns.coordinateSquareSumFDeriv_zero {n : ℕ} : coordinateSquareSumFDeriv 0 = 0

The coordinate formula for the first derivative of the coordinate square-sum vanishes at the origin.

theorem ViscositySolns.differentiableWithinAt_coordinateSquareSumFDeriv_zero {n : ℕ} : DifferentiableWithinAt ℝ coordinateSquareSumFDeriv Set.univ 0

The coordinate formula for the first derivative of the coordinate square-sum is differentiable at the origin.

def ViscositySolns.coordinateQuarticFDeriv {n : ℕ} (x : Point n) : Point n →L[ℝ] ℝ

The derivative of the coordinate quartic, written in terms of the square-sum and its derivative.

Equations

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

theorem ViscositySolns.hasFDerivWithinAt_coordinateQuarticFDeriv_zero {n : ℕ} : HasFDerivWithinAt coordinateQuarticFDeriv 0 Set.univ 0

At the origin, the derivative of the coordinate-quartic derivative formula is zero.

theorem ViscositySolns.hasFDerivWithinAt_coordinateQuartic {n : ℕ} (x : Point n) : HasFDerivWithinAt coordinateQuartic (coordinateQuarticFDeriv x) Set.univ x

At every point, the coordinate quartic has the first Fréchet derivative given by coordinateQuarticFDeriv.

theorem ViscositySolns.fderivWithin_coordinateQuartic_univ_zero {n : ℕ} : fderivWithin ℝ coordinateQuartic Set.univ 0 = 0

At the origin, the coordinate quartic has zero first Fréchet derivative.

theorem ViscositySolns.hasFDerivWithinAt_fderivWithin_coordinateQuartic_univ_zero {n : ℕ} : HasFDerivWithinAt (fderivWithin ℝ coordinateQuartic Set.univ) 0 Set.univ 0

At the origin, the first-derivative map of the coordinate quartic has zero Fréchet derivative.

theorem ViscositySolns.fderivWithin_fderivWithin_coordinateQuartic_univ_zero {n : ℕ} : fderivWithin ℝ (fderivWithin ℝ coordinateQuartic Set.univ) Set.univ 0 = 0

At the origin, the second Fréchet derivative of the coordinate quartic is zero.

theorem ViscositySolns.coordinateQuartic_pos_of_ne_zero {n : ℕ} {x : Point n} (hx : x ≠ 0) : 0 < coordinateQuartic x

The coordinate quartic is strictly positive away from the origin.

theorem ViscositySolns.coordinateQuartic_isLittleO_norm_sq {n : ℕ} : (fun (x : Point n) => coordinateQuartic x) =o[nhds 0] fun (x : Point n) => ‖x‖ ^ 2

The coordinate quartic is fourth order at the origin.

In quantified mathematical form,

(∑ i, x_i^2)^2 = o(|x|^2) as x -> 0.

theorem ViscositySolns.hasSecondOrderExpansionWithin_coordinateQuartic_zero {n : ℕ} {C : Set (Point n)} : HasSecondOrderExpansionWithin C coordinateQuartic 0 { gradient := 0, hessian := 0 }

At the origin, the coordinate quartic has zero value, zero gradient, and zero Hessian in the second-order expansion sense used by semijets.

noncomputable def ViscositySolns.coordinateQuarticJetAt {n : ℕ} (x : Point n) : Jet n

The canonical second-order jet of the coordinate quartic at a point.

In quantified mathematical form, this is the pair whose first component is the Fréchet derivative of x ↦ (∑ i, x_i^2)^2 at x, and whose second component is the Fréchet derivative at x of the first-derivative map. Both derivatives are converted from mathlib's continuous-linear-map form to the coordinate gradient and Hessian used by semijets.

Equations

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

@[simp]

theorem ViscositySolns.coordinateQuarticJetAt_zero {n : ℕ} : coordinateQuarticJetAt 0 = 0

The canonical coordinate-quartic jet at the origin is the zero jet.

theorem ViscositySolns.coordinateQuarticJetAt_hessian_isHermitian {n : ℕ} (x : Point n) : Matrix.IsHermitian (coordinateQuarticJetAt x).hessian

The Hessian component of the canonical coordinate-quartic jet is Hermitian at every point.

theorem ViscositySolns.hasSecondOrderExpansionWithin_coordinateQuartic_univ {n : ℕ} (x : Point n) : HasSecondOrderExpansionWithin Set.univ coordinateQuartic x (coordinateQuarticJetAt x)

At every point, the coordinate quartic has the second-order expansion given by its canonical first and second Fréchet derivatives.

theorem ViscositySolns.continuous_coordinateQuarticJetAt {n : ℕ} : Continuous coordinateQuarticJetAt

The canonical coordinate-quartic jet depends continuously on the base point.

theorem ViscositySolns.tendsto_coordinateQuarticJetAt_hessian_zero {n : ℕ} : Filter.Tendsto (fun (x : Point n) => (coordinateQuarticJetAt x).hessian) (nhds 0) (nhds 0)

As x -> 0, the Hessian component of the canonical coordinate-quartic jet tends to zero.

theorem ViscositySolns.tendsto_coordinateQuarticJetAt_gradient_zero {n : ℕ} : Filter.Tendsto (fun (x : Point n) => (coordinateQuarticJetAt x).gradient) (nhds 0) (nhds 0)

As x -> 0, the gradient component of the canonical coordinate-quartic jet tends to zero.