English
In dimension one, torus integral coincides with circle integral under a natural identification between ℂ and Fin 1 → ℂ.
Русский
В размерности 1 торус-интеграл совпадает с circle integral через естественное соответствие ℂ и Fin 1 → ℂ.
LaTeX
$$$\operatorname{torusIntegral}(f,c,R) = \operatorname{circleIntegral}(\text{...}, c_0, R_0)$$$
Lean4
/-- In dimension one, `torusIntegral` is the same as `circleIntegral`
(up to the natural equivalence between `ℂ` and `Fin 1 → ℂ`). -/
theorem torusIntegral_dim1 (f : (ℂ¹) → E) (c : ℂ¹) (R : ℝ¹) :
(∯ x in T(c, R), f x) = ∮ z in C(c 0, R 0), f fun _ => z :=
by
have H₁ : (((MeasurableEquiv.funUnique _ _).symm) ⁻¹' Icc 0 fun _ => 2 * π) = Icc 0 (2 * π) :=
(OrderIso.funUnique (Fin 1) ℝ).symm.preimage_Icc _ _
have H₂ : torusMap c R = fun θ _ ↦ circleMap (c 0) (R 0) (θ 0) :=
by
ext θ i : 2
rw [Subsingleton.elim i 0]; rfl
rw [torusIntegral, circleIntegral, intervalIntegral.integral_of_le Real.two_pi_pos.le,
Measure.restrict_congr_set Ioc_ae_eq_Icc, ←
((volume_preserving_funUnique (Fin 1) ℝ).symm _).setIntegral_preimage_emb (MeasurableEquiv.measurableEmbedding _),
H₁, H₂]
simp [circleMap_zero]
