English
If a point x lies in the integer complement, then x is nonzero.
Русский
Если точка x лежит в дополнении целых, то x ≠ 0.
LaTeX
$$$x \\in \\mathbb{C}_{\\mathbb{Z}} \\Rightarrow x \\neq 0.$$$
Lean4
/-- If a function `f` `IsConservativeOn` on a disk of center `c`, then for points `z` in this disk,
the wedge integral from `c` to `z` is additive under a detour through a nearby point `w`. -/
theorem eventually_nhds_wedgeIntegral_sub_wedgeIntegral (hf : IsConservativeOn f (ball c r)) :
∀ᶠ w in 𝓝 z, wedgeIntegral c w f - wedgeIntegral c z f = wedgeIntegral z w f :=
by
refine eventually_nhds_iff_ball.mpr ⟨r - dist z c, by simpa using hz, fun w w_in_z_ball ↦ ?_⟩
set I₁ := ∫ x in c.re..w.re, f (x + c.im * I)
set I₂ := I • ∫ y in c.im..w.im, f (w.re + y * I)
set I₃ := ∫ x in c.re..z.re, f (x + c.im * I)
set I₄ := I • ∫ y in c.im..z.im, f (z.re + y * I)
set I₅ := ∫ x in z.re..w.re, f (x + z.im * I)
set I₆ := I • ∫ y in z.im..w.im, f (w.re + y * I)
set I₇ := ∫ x in z.re..w.re, f (x + c.im * I)
set I₈ := I • ∫ y in c.im..z.im, f (w.re + y * I)
have z_ball : ball z (r - dist z c) ⊆ ball c r := ball_subset_ball' (by simp)
have w_mem : w ∈ ball c r := mem_of_subset_of_mem z_ball w_in_z_ball
have integrableHoriz (a₁ a₂ b : ℝ) (ha₁ : a₁ + b * I ∈ ball c r) (ha₂ : a₂ + b * I ∈ ball c r) :
IntervalIntegrable (fun x ↦ f (x + b * I)) volume a₁ a₂ :=
((f_cont.mono (mem_ball_of_map_re_aux ha₁ ha₂)).comp (by fun_prop) (mapsTo_image _ _)).intervalIntegrable
have integrableVert (a b₁ b₂ : ℝ) (hb₁ : a + b₁ * I ∈ ball c r) (hb₂ : a + b₂ * I ∈ ball c r) :
IntervalIntegrable (fun y ↦ f (a + y * I)) volume b₁ b₂ :=
((f_cont.mono (mem_ball_of_map_im_aux₁ hb₁ hb₂)).comp (by fun_prop) (mapsTo_image _ _)).intervalIntegrable
have hI₁ : I₁ = I₃ + I₇ :=
by
rw [intervalIntegral.integral_add_adjacent_intervals] <;> apply integrableHoriz
· exact re_add_im_mul_mem_ball <| mem_ball_self (pos_of_mem_ball hz)
· exact re_add_im_mul_mem_ball hz
· exact re_add_im_mul_mem_ball hz
· exact re_add_im_mul_mem_ball w_mem
have hI₂ : I₂ = I₈ + I₆ :=
by
rw [← smul_add, intervalIntegral.integral_add_adjacent_intervals] <;> apply integrableVert
· exact re_add_im_mul_mem_ball w_mem
· exact mem_of_subset_of_mem z_ball (re_add_im_mul_mem_ball w_in_z_ball)
· exact mem_of_subset_of_mem z_ball (re_add_im_mul_mem_ball w_in_z_ball)
· simpa using w_mem
have hI₀ : I₇ - I₅ + I₈ - I₄ = 0 :=
by
have wzInBall : w.re + z.im * I ∈ ball c r := mem_of_subset_of_mem z_ball (re_add_im_mul_mem_ball w_in_z_ball)
have wcInBall : w.re + c.im * I ∈ ball c r := re_add_im_mul_mem_ball w_mem
have hU : Rectangle (z.re + c.im * I) (w.re + z.im * I) ⊆ ball c r :=
(convex_ball c r).rectangle_subset (re_add_im_mul_mem_ball hz) wzInBall (by simpa using hz)
(by simpa using wcInBall)
simpa [← add_eq_zero_iff_eq_neg, wedgeIntegral_add_wedgeIntegral_eq] using hf (z.re + c.im * I) (w.re + z.im * I) hU
grind [wedgeIntegral]
/- The horizontal integral of `f` from `z` to `z.re + w.im * I` is equal to `(w - z).re * f z`
up to `o(w - z)`, as `w` tends to `z`. -/
