English
The derivative of the circle transform is locally bounded: around any x inside the ball, there is a neighborhood where |circleTransformDeriv| is bounded by some constant B.
Русский
Производная circleTransform ограничена локально: вокруг любой точки x внутри шара найдётся окрестность, где модуль circleTransformDeriv ≤ B.
LaTeX
$$$$ \\exists B,\\exists \\varepsilon>0\\ s.t.\\ \\forall t\\in\\mathbb{R},\\ \\forall y\\in B(x,\\varepsilon),\\|\\mathrm{circleTransformDeriv}(R,z,y,f,t)\\| \\le B. $$$$
Lean4
/-- The derivative of a `circleTransform` is locally bounded. -/
theorem circleTransformDeriv_bound {R : ℝ} (hR : 0 < R) {z x : ℂ} {f : ℂ → ℂ} (hx : x ∈ ball z R)
(hf : ContinuousOn f (sphere z R)) :
∃ B ε : ℝ, 0 < ε ∧ ball x ε ⊆ ball z R ∧ ∀ (t : ℝ), ∀ y ∈ ball x ε, ‖circleTransformDeriv R z y f t‖ ≤ B :=
by
obtain ⟨r, hr, hrx⟩ := exists_lt_mem_ball_of_mem_ball hx
obtain ⟨ε', hε', H⟩ := exists_ball_subset_ball hrx
obtain ⟨⟨⟨a, b⟩, ⟨ha, hb⟩⟩, hab⟩ := norm_circleTransformBoundingFunction_le hr (pos_of_mem_ball hrx).le z
let V : ℝ → ℂ → ℂ := fun θ w => circleTransformDeriv R z w (fun _ => 1) θ
obtain ⟨X, -, HX2⟩ := (isCompact_sphere z R).exists_isMaxOn (NormedSpace.sphere_nonempty.2 hR.le) hf.norm
refine ⟨‖V b a‖ * ‖f X‖, ε', hε', H.trans (ball_subset_ball hr.le), fun y v hv ↦ ?_⟩
obtain ⟨y1, hy1, hfun⟩ := Periodic.exists_mem_Ico₀ (circleTransformDeriv_periodic R z v f) Real.two_pi_pos y
have hy2 : y1 ∈ [[0, 2 * π]] := Icc_subset_uIcc <| Ico_subset_Icc_self hy1
simp only [isMaxOn_iff, mem_sphere_iff_norm] at HX2
have :=
mul_le_mul (hab ⟨⟨v, y1⟩, ⟨ball_subset_closedBall (H hv), hy2⟩⟩)
(HX2 (circleMap z R y1) (circleMap_mem_sphere z hR.le y1)) (norm_nonneg _) (norm_nonneg _)
rw [hfun]
simpa [V, circleTransformBoundingFunction, circleTransformDeriv, mul_assoc] using this
