One-Dimensional Continuous Linear Maps

In the one-dimensional case ℝ →L[ℝ] ℝ, every continuous linear map is scalar multiplication by some constant a ∈ ℝ.

smul，scalar multiplication, typeclass behind • in LEAN. We define smulCLM a as the continuous linear map x ↦ a·x. First we establish key properties:

• Operator norm: ‖smulCLM a‖ = |a|
• Composition: (smulCLM a) ∘ (smulCLM b) = smulCLM (a·b)
• Subtraction: smulCLM a - smulCLM b = smulCLM (a - b)
• Injectivity: smulCLM a is injective iff a ≠ 0

These lemmas enable working with the radii polynomial theorem in ℝ, where the approximate inverse A and derivative Df(x̄) are both scalar CLMs.

@[reducible, inline]

noncomputable abbrev smulCLM (a : ℝ) : ℝ →L[ℝ] ℝ

A scalar as a continuous linear map ℝ →L[ℝ] ℝ.

For a ∈ ℝ, smulCLM a is the map x ↦ a·x

This is noncomputable because of ℝ.

Equations

• smulCLM a = a • ContinuousLinearMap.id ℝ ℝ

@[simp]

theorem smulCLM_apply (a x : ℝ) : (smulCLM a) x = a * x

Evaluation: (smulCLM a)(x) = a * x

theorem norm_smulCLM (a : ℝ) : ‖smulCLM a‖ = |a|

Operator norm of scalar multiplication equals absolute value.

‖smulCLM a‖_{op} = |a|

This is the key fact enabling norm computations in 1D.

theorem id_eq_smulCLM_one : ContinuousLinearMap.id ℝ ℝ = smulCLM 1

The identity map is smulCLM 1

theorem smulCLM_comp (a b : ℝ) : (smulCLM a).comp (smulCLM b) = smulCLM (a * b)

Composition of scalar CLMs is multiplication of scalars.

(smulCLM a) ∘ (smulCLM b) = smulCLM (a * b)

Used to compute A ∘ Df(x̄) when both are scalar multiplications.

theorem smulCLM_sub (a b : ℝ) : smulCLM a - smulCLM b = smulCLM (a - b)

Subtraction of scalar CLMs.

smulCLM a - smulCLM b = smulCLM (a - b)

Used to compute Df(c) - Df(x̄) = smulCLM(2c) - smulCLM(2x̄) = smulCLM(2(c - x̄)).

theorem id_sub_smulCLM (a : ℝ) : ContinuousLinearMap.id ℝ ℝ - smulCLM a = smulCLM (1 - a)

Identity minus scalar CLM.

I - smulCLM a = smulCLM (1 - a)

Used to compute I - A∘Df(x̄) for the Z₀ bound.

theorem smulCLM_injective {a : ℝ} (ha : a ≠ 0) : Function.Injective ⇑(smulCLM a)

Injectivity of scalar multiplication.

smulCLM a is injective iff a ≠ 0.

Required hypothesis for Proposition 2.3.1 (fixed point ↔ zero equivalence).

Fréchet Derivatives

For f(x) = x² - 2, we have Df(x) = smulCLM (2x).

theorem fderiv_sq (x : ℝ) : fderiv ℝ (fun (y : ℝ) => y ^ 2) x = smulCLM (2 * x)

The Fréchet derivative of x² at x is multiplication by 2x.

For f(y) = y², we have Df(x) : v ↦ 2x·v, i.e., Df(x) = smulCLM(2x).

This follows from the power rule: D[y^n] = n·y^(n-1)·id.

theorem fderiv_sq_sub_const (x c : ℝ) : fderiv ℝ (fun (y : ℝ) => y ^ 2 - c) x = smulCLM (2 * x)

The Fréchet derivative of x² - c

theorem differentiable_sq_sub_const (c : ℝ) : Differentiable ℝ fun (y : ℝ) => y ^ 2 - c

Example 2.4.5: Bounds Verification

All bounds use exact rational arithmetic for formal verification.

Parameter definitions

@[reducible, inline]

noncomputable abbrev ex_f : ℝ → ℝ

Equations

• ex_f x = x ^ 2 - 2

@[reducible, inline]

noncomputable abbrev ex_xBar : ℝ

Equations

• ex_xBar = 13 / 10

@[reducible, inline]

noncomputable abbrev ex_A : ℝ →L[ℝ] ℝ

Equations

• ex_A = smulCLM (19 / 50)

@[reducible, inline]

noncomputable abbrev ex_Y₀ : ℝ

Equations

• ex_Y₀ = 3 / 25

@[reducible, inline]

noncomputable abbrev ex_Z₀ : ℝ

Equations

• ex_Z₀ = 3 / 250

@[reducible, inline]

noncomputable abbrev ex_Z₂ : ℝ → ℝ

Equations

• ex_Z₂ x✝ = 19 / 25

@[reducible, inline]

noncomputable abbrev ex_r₀ : ℝ

Equations

• ex_r₀ = 3 / 20

Bound verification lemmas

theorem ex_bound_Y₀ : ‖ex_A (ex_f ex_xBar)‖ ≤ ex_Y₀

eq. 2.14: ‖A(f(x̄))‖ ≤ Y₀

theorem ex_bound_Z₀ : ‖ContinuousLinearMap.id ℝ ℝ - ex_A.comp (fderiv ℝ ex_f ex_xBar)‖ ≤ ex_Z₀

eq. 2.15: ‖I - A ∘ Df(x̄)‖ ≤ Z₀

theorem ex_bound_Z₂ {c : ℝ} (r : ℝ) (hc : c ∈ Metric.closedBall ex_xBar r) : ‖ex_A.comp (fderiv ℝ ex_f c - fderiv ℝ ex_f ex_xBar)‖ ≤ ex_Z₂ r * r

eq. 2.16: ‖A ∘ [Df(c) - Df(x̄)]‖ ≤ Z₂(r) · r for c ∈ B̄ᵣ(x̄)

theorem ex_radii_poly_neg : radiiPolynomial ex_Y₀ ex_Z₀ ex_Z₂ ex_r₀ < 0

The radii polynomial is negative at r₀ = 0.15

theorem ex_r₀_pos : 0 < ex_r₀

r₀ is positive

theorem ex_A_inj : Function.Injective ⇑ex_A

A is injective

theorem ex_f_diff : Differentiable ℝ ex_f

f is differentiable

Main Theorem Application

Apply simple_radii_polynomial_theorem_same_space from RadiiPolyGeneral.

theorem ball_elements_pos (y : ℝ) (hy : y ∈ Metric.closedBall ex_xBar ex_r₀) : 0 < y

Elements in the ball are positive (ball is [1.15, 1.45])

theorem fderiv_invertible_of_pos {y : ℝ} (hy : 0 < y) : (fderiv ℝ ex_f y).IsInvertible

Df(y) is invertible when y > 0

theorem example_2_4_5 : ∃! xTilde : ℝ, xTilde ∈ Metric.closedBall ex_xBar ex_r₀ ∧ ex_f xTilde = 0 ∧ (fderiv ℝ ex_f xTilde).IsInvertible

Example 2.4.5: There exists a unique x̃ ∈ B̄_{3/20}(13/10) with x̃² = 2.

Furthermore, Df(x̃) is invertible, so x̃ is a nondegenerate zero.

theorem example_2_4_5_sqrt2 : ∃! xTilde : ℝ, xTilde ∈ Metric.closedBall ex_xBar ex_r₀ ∧ xTilde ^ 2 = 2

Corollary: The zero is √2 (or -√2, but our ball only contains √2)