Stage 2, route A: finite-dimensional differentiation

This file isolates the Hessian/integration route toward O3.belowGeometry. It deliberately does not export the frozen theorem until the singular-line integration argument is complete.

noncomputable def O3.Stage2RouteA.linePower (p : ℝ) {d : ℕ} (x h : Point d) (t : ℝ) : ℝ

The power sum along an affine line.

Equations

• O3.Stage2RouteA.linePower p x h t = O3.lpPower p (x + t • h)

noncomputable def O3.Stage2RouteA.linePowerDerivative (p : ℝ) {d : ℕ} (x h : Point d) (t : ℝ) : ℝ

The directional pairing with the unnormalised power-duality map.

Equations

• O3.Stage2RouteA.linePowerDerivative p x h t = p * O3.pairing (O3.powerDualityMap p (x + t • h)) h

theorem O3.Stage2RouteA.hasDerivAt_abs_affine_rpow {p a b t : ℝ} (hp : 1 < p) : HasDerivAt (fun (s : ℝ) => |a + s * b| ^ p) (p * |a + t * b| ^ (p - 2) * (a + t * b) * b) t

theorem O3.Stage2RouteA.hasDerivAt_linePower {p : ℝ} (hp : 1 < p) {d : ℕ} (x h : Point d) (t : ℝ) : HasDerivAt (linePower p x h) (linePowerDerivative p x h t) t

theorem O3.Stage2RouteA.lpNorm_sq_eq_lpPower_rpow {p : ℝ} (hp : p ≠ 0) {d : ℕ} (z : Point d) : lpNorm p z ^ 2 = lpPower p z ^ (2 / p)

The squared norm written as a single real power of the finite power sum.

noncomputable def O3.Stage2RouteA.lineEnergy (p : ℝ) {d : ℕ} (x h : Point d) (t : ℝ) : ℝ

The one-variable restriction of x ↦ (1/2)‖x‖_p².

Equations

• O3.Stage2RouteA.lineEnergy p x h t = 1 / 2 * O3.Stage2RouteA.linePower p x h t ^ (2 / p)

theorem O3.Stage2RouteA.lineEnergy_eq_quadraticRegularizer {p : ℝ} (hp : p ≠ 0) {d : ℕ} (x h : Point d) (t : ℝ) : lineEnergy p x h t = quadraticRegularizer p 0 (x + t • h)

theorem O3.Stage2RouteA.lpPower_rpow_two_div_sub_one_eq {p : ℝ} (hp : p ≠ 0) {d : ℕ} {z : Point d} (hz : z ≠ 0) : lpPower p z ^ (2 / p - 1) = lpNorm p z ^ (2 - p)

theorem O3.Stage2RouteA.hasDerivAt_lineEnergy_of_ne_zero {p : ℝ} (hp : 1 < p) {d : ℕ} (x h : Point d) (t : ℝ) (hz : x + t • h ≠ 0) : HasDerivAt (lineEnergy p x h) (pairing (dualityMap p (x + t • h)) h) t

theorem O3.Stage2RouteA.hasDerivAt_scalarJ_of_ne_zero {p u : ℝ} (hu : u ≠ 0) : HasDerivAt (Experimental.scalarJ p) ((p - 1) * |u| ^ (p - 2)) u

Away from the scalar singularity, the derivative of |u|^(p-2)u has its expected exact coefficient.

theorem O3.Stage2RouteA.hasDerivAt_scalarJ_zero {q : ℝ} (hq : 2 < q) : HasDerivAt (Experimental.scalarJ q) 0 0

For exponents above two, the unnormalised duality map is differentiable also at the scalar zero, with derivative zero.

theorem O3.Stage2RouteA.hasDerivAt_scalarJ_above_two {q u : ℝ} (hq : 2 < q) : HasDerivAt (Experimental.scalarJ q) ((q - 1) * |u| ^ (q - 2)) u

noncomputable def O3.Stage2RouteA.weightedSquareSum (p : ℝ) {d : ℕ} (x h : Point d) (t : ℝ) : ℝ

The weighted quadratic form that appears in the Hessian.

Equations

• O3.Stage2RouteA.weightedSquareSum p x h t = ∑ i : Fin d, |(x + t • h) i| ^ (p - 2) * h i ^ 2

noncomputable def O3.Stage2RouteA.linePowerPair (p : ℝ) {d : ℕ} (x h : Point d) (t : ℝ) : ℝ

The unnormalised duality pairing along a line.

Equations

• O3.Stage2RouteA.linePowerPair p x h t = O3.pairing (O3.powerDualityMap p (x + t • h)) h

theorem O3.Stage2RouteA.hasDerivAt_scalarJ_affine {p a b t : ℝ} (hz : a + t * b ≠ 0) : HasDerivAt (fun (s : ℝ) => Experimental.scalarJ p (a + s * b)) ((p - 1) * |a + t * b| ^ (p - 2) * b) t

theorem O3.Stage2RouteA.hasDerivAt_linePowerPair_of_coordinates_ne_zero {p : ℝ} {d : ℕ} (x h : Point d) (t : ℝ) (hz : ∀ (i : Fin d), (x + t • h) i ≠ 0) : HasDerivAt (linePowerPair p x h) ((p - 1) * weightedSquareSum p x h t) t

theorem O3.Stage2RouteA.hasDerivAt_linePowerPair_above_two {q : ℝ} (hq : 2 < q) {d : ℕ} (x h : Point d) (t : ℝ) : HasDerivAt (linePowerPair q x h) ((q - 1) * weightedSquareSum q x h t) t

For q > 2, the Hessian's coordinatewise power term is differentiable even when coordinates cross zero.

theorem O3.Stage2RouteA.pairing_dualityMap_smul {q : ℝ} (hq : 1 < q) {d : ℕ} (a : ℝ) (h : Point d) : pairing (dualityMap q (a • h)) h = a * lpNorm q h ^ 2

Exact radial formula for the normalized duality pairing.

theorem O3.Stage2RouteA.line_duality_pair_eq_affine_of_zero {q : ℝ} (hq : 1 < q) {d : ℕ} (x h : Point d) (t : ℝ) (hz : x + t • h = 0) : (fun (s : ℝ) => pairing (dualityMap q (x + s • h)) h) = fun (s : ℝ) => (s - t) * lpNorm q h ^ 2

At the unique whole-vector zero on an affine line, the actual normalized duality pairing is locally (indeed globally) affine in the line parameter.

theorem O3.Stage2RouteA.hasDerivAt_line_duality_pair_at_zero {q : ℝ} (hq : 1 < q) {d : ℕ} (x h : Point d) (t : ℝ) (hz : x + t • h = 0) : HasDerivAt (fun (s : ℝ) => pairing (dualityMap q (x + s • h)) h) (lpNorm q h ^ 2) t

noncomputable def O3.Stage2RouteA.lineGradientFormula (p : ℝ) {d : ℕ} (x h : Point d) (t : ℝ) : ℝ

Algebraic nonzero-vector formula for the directional derivative of the squared norm. Unlike dualityMap, it has no conditional branch.

Equations

• O3.Stage2RouteA.lineGradientFormula p x h t = O3.Stage2RouteA.linePower p x h t ^ (2 / p - 1) * O3.Stage2RouteA.linePowerPair p x h t

theorem O3.Stage2RouteA.lineGradientFormula_eq_duality_pair {p : ℝ} (hp : p ≠ 0) {d : ℕ} (x h : Point d) (t : ℝ) (hz : x + t • h ≠ 0) : lineGradientFormula p x h t = pairing (dualityMap p (x + t • h)) h

theorem O3.Stage2RouteA.hasDerivAt_lineGradientFormula_of_coordinates_ne_zero {p : ℝ} (hp : 1 < p) {d : ℕ} (x h : Point d) (t : ℝ) (hzvec : x + t • h ≠ 0) (hz : ∀ (i : Fin d), (x + t • h) i ≠ 0) : HasDerivAt (lineGradientFormula p x h) ((2 - p) * linePower p x h t ^ (2 / p - 2) * linePowerPair p x h t ^ 2 + (p - 1) * linePower p x h t ^ (2 / p - 1) * weightedSquareSum p x h t) t

Exact Hessian formula at points where the vector and all coordinates avoid the real-power singularities.

theorem O3.Stage2RouteA.hasDerivAt_lineGradientFormula_above_two_of_ne_zero {q : ℝ} (hq : 2 < q) {d : ℕ} (x h : Point d) (t : ℝ) (hzvec : x + t • h ≠ 0) : HasDerivAt (lineGradientFormula q x h) ((2 - q) * linePower q x h t ^ (2 / q - 2) * linePowerPair q x h t ^ 2 + (q - 1) * linePower q x h t ^ (2 / q - 1) * weightedSquareSum q x h t) t

Above two, the same exact normalized Hessian formula needs only the whole vector to be nonzero; scalar zero coordinates are covered by hasDerivAt_scalarJ_zero.

theorem O3.Stage2RouteA.lineGradientFormula_deriv_le_above_two {q : ℝ} (hq : 2 < q) {d : ℕ} (x h : Point d) (t : ℝ) (hzvec : x + t • h ≠ 0) : (2 - q) * linePower q x h t ^ (2 / q - 2) * linePowerPair q x h t ^ 2 + (q - 1) * linePower q x h t ^ (2 / q - 1) * weightedSquareSum q x h t ≤ (q - 1) * lpNorm q h ^ 2

theorem O3.Stage2RouteA.exists_hasDerivAt_line_duality_pair_le_above_two {q : ℝ} (hq : 2 < q) {d : ℕ} (x h : Point d) (t : ℝ) : ∃ (v : ℝ), HasDerivAt (fun (s : ℝ) => pairing (dualityMap q (x + s • h)) h) v t ∧ v ≤ (q - 1) * lpNorm q h ^ 2

Every line parameter admits an exact derivative of the actual normalized duality pairing, together with the sharp (q-1) upper bound. The proof splits only on the whole-vector zero; scalar coordinate zeros are already native.

theorem O3.Stage2RouteA.weightedTerm_le_hessianFormula {p : ℝ} (hp2 : p ≤ 2) {d : ℕ} (x h : Point d) (t : ℝ) : (p - 1) * linePower p x h t ^ (2 / p - 1) * weightedSquareSum p x h t ≤ (2 - p) * linePower p x h t ^ (2 / p - 2) * linePowerPair p x h t ^ 2 + (p - 1) * linePower p x h t ^ (2 / p - 1) * weightedSquareSum p x h t

The first Hessian term is nonnegative throughout the frozen range p ≤ 2; hence only the weighted Hölder term remains for the pointwise lower bound.

theorem O3.Stage2RouteA.weightedSquareSum_two_eq {d : ℕ} (x h : Point d) (t : ℝ) : weightedSquareSum 2 x h t = lpNorm 2 h ^ 2

At the endpoint p = 2, the weighted Hölder bridge is an identity.

noncomputable def O3.Stage2RouteA.WeightedHolderResidual : Prop

The exact remaining pointwise inequality in route A for 1 < p < 2. It is kept as a transparent residual proposition, not as an assumption of any proved declaration.

Equations

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