Nested cylinders and absorption for the interior analyticity induction #
Two elementary facts used in the proof of thm:analytic:interior. The region of depth τ is
{|x| < R' + (1 - τ) d} × [s₁ - (1 - τ) d², s₂]. A backward window of radius
ρ = θ τ d / (k + 1) around a point of depth τ lies in the region of depth
τ (1 - θ / (k + 1)), and moving to that depth costs at most a factor 2 on the weights
(τ d)^j, j ≤ k + 2. The second fact is the limit form of the absorption step.
theorem
CIV.kahane_window_subset_deeper
{R' d s₁ s₂ τ θ : ℝ}
(hd : 0 < d)
(hd1 : d ≤ 1)
(hτ : 0 < τ)
(hτ1 : τ ≤ 1)
(hθ : 0 < θ)
(hθ4 : θ ≤ 1 / 4)
(k : ℕ)
:
0 < θ * τ * d / (↑k + 1) ∧ θ * τ * d / (↑k + 1) ≤ 1 ∧ 0 < τ * (1 - θ / (↑k + 1)) ∧ τ * (1 - θ / (↑k + 1)) ≤ τ ∧ (∀ (x : CKN.Foundation.Parabolic.Vec3) (t : ℝ),
CKN.Foundation.Parabolic.vec3EuclideanNorm x < R' + (1 - τ) * d →
s₁ - (1 - τ) * d ^ 2 ≤ t →
t ≤ s₂ →
∀
z ∈
{y : CKN.Foundation.Parabolic.Vec3 | CKN.Foundation.Parabolic.vec3EuclideanNorm (y - x) ≤ θ * τ * d / (↑k + 1)} ×ˢ Set.Icc (t - (θ * τ * d / (↑k + 1)) ^ 2) t,
CKN.Foundation.Parabolic.vec3EuclideanNorm z.1 < R' + (1 - τ * (1 - θ / (↑k + 1))) * d ∧ s₁ - (1 - τ * (1 - θ / (↑k + 1))) * d ^ 2 ≤ z.2 ∧ z.2 ≤ s₂) ∧ ∀ j ≤ k + 2, (τ * d) ^ j ≤ 2 * (τ * (1 - θ / (↑k + 1)) * d) ^ j
A backward window of radius θ τ d / (k + 1) around a point of depth τ lies in the region
of depth τ (1 - θ / (k + 1)), and the weights change by at most a factor 2 up to order
k + 2.