English
Let c ∈ ℂ, R ∈ ℝ, and f1, f2: ℂ → E with E a normed additive group. If f1 and f2 agree off a codiscrete subset of the circle { z ∈ ℂ : |z − c| = |R| } and f1 is circle-integrable on the circle of center c and radius R, then f2 is also circle-integrable on that circle.
Русский
Пусть c ∈ ℂ, R ∈ ℝ, и f1, f2: ℂ → E, где E — нормированная абелевай группа. Если f1 и f2 совпадают на окружности { z ∈ ℂ : |z − c| = |R| } за исключением подмножества, кодискретного внутри этой окружности, и f1 кругово интегрируема вдоль окружности с центром c и радиусом R, то и f2 кругово интегрируема вдоль той же окружности.
LaTeX
$$$\\text{CircleIntegrable}(f_1,c,R)\\;\\Rightarrow\\;\\text{CircleIntegrable}(f_2,c,R)$ \n\\quad \\text{whenever } f_1 =\\!\\!\\!\\!_{codiscreteWithin(\\mathrm{sphere}\\;c\\;|R|)} f_2, \n\\text{(with }R\\text{ arbitrary; the degenerate radius }R=0\\text{ is trivial).}$$$
Lean4
/-- Circle integrability is invariant when functions change along discrete sets. -/
theorem congr_codiscreteWithin {c : ℂ} {R : ℝ} {f₁ f₂ : ℂ → E} (hf : f₁ =ᶠ[codiscreteWithin (Metric.sphere c |R|)] f₂)
(hf₁ : CircleIntegrable f₁ c R) : CircleIntegrable f₂ c R :=
by
by_cases hR : R = 0
· simp [hR]
apply (intervalIntegrable_congr_codiscreteWithin _).1 hf₁
rw [eventuallyEq_iff_exists_mem]
exact
⟨(circleMap c R) ⁻¹' {z | f₁ z = f₂ z},
codiscreteWithin.mono (by simp only [Set.subset_univ]) (circleMap_preimage_codiscrete hR hf), by tauto⟩
