Radii for unique-continuation propagation

The radii in thm:uc increase from the initial Gaussian ball toward the full source ball.

noncomputable def ESS.ucRadiusFraction : ℝ

The fraction of each remaining radius reached by one Gaussian continuation step.

Equations

• ESS.ucRadiusFraction = 3 / 8 * √(2 / 100)

noncomputable def ESS.ucRadius (R : ℝ) (n : ℕ) : ℝ

The radius reached after n continuation steps in thm:uc.

Equations

• ESS.ucRadius R n = R * (1 - (1 - ESS.ucRadiusFraction) ^ (n + 1))

theorem ESS.ucRadiusFraction_pos_lt_one : 0 < ucRadiusFraction ∧ ucRadiusFraction < 1

The continuation fraction lies strictly between zero and one.

theorem ESS.ucRadius_zero (R : ℝ) : ucRadius R 0 = ucRadiusFraction * R

The first radius equals the Gaussian lemma's initial spatial radius.

theorem ESS.ucRadius_succ (R : ℝ) (n : ℕ) : ucRadius R (n + 1) = ucRadius R n + ucRadiusFraction * (R - ucRadius R n)

The radii follow the affine recurrence in the proof of thm:uc.

theorem ESS.ucRadius_pos_lt (R : ℝ) (hR : 0 < R) (n : ℕ) : 0 < ucRadius R n ∧ ucRadius R n < R

Every continuation radius is positive and below the original radius.

theorem ESS.ucRadius_eventually_covers (R d : ℝ) (hR : 0 < R) (hd : d < R) : ∃ (n : ℕ), d < ucRadius R n

Every point in the source ball lies inside some continuation radius.

theorem ESS.ucRadius_initial_le (R : ℝ) (hR : 0 < R) (n : ℕ) : ucRadius R 0 ≤ ucRadius R n

Every radius is at least the initial Gaussian radius.

theorem ESS.uc_radius_step_center (R : ℝ) (hR : 0 < R) (n : ℕ) (x : CKN.Foundation.Parabolic.Vec3) (hinner : ucRadius R n ≤ CKN.Foundation.Parabolic.vec3EuclideanNorm x) (houter : CKN.Foundation.Parabolic.vec3EuclideanNorm x < ucRadius R (n + 1)) : ∃ x₀ ∈ CKN.Foundation.Parabolic.vec3Ball 0 (ucRadius R n), x₀ ∈ CKN.Foundation.Parabolic.vec3Ball 0 R ∧ x ∈ CKN.Foundation.Parabolic.vec3Ball x₀ (ucRadiusFraction * (R - CKN.Foundation.Parabolic.vec3EuclideanNorm x₀))

A point in the next radius lies within the Gaussian reach of a center strictly inside the current radius.