English
A recurrence formula expresses torusIntegral f on a product torus in terms of torusIntegral on a shifted torus and a circle integral.
Русский
Рекуррентная формула выражает torusIntegral через torusIntegral на сдвинутом торусе и circleIntegral.
LaTeX
$$$\operatorname{torusIntegral}(f,c,R) = \oint x ∈ C(c_i,R_i), \operatorname{torusIntegral}(f(i.insertNth x y), c ∘ i.succAbove, R ∘ i.succAbove) \, dy$$$
Lean4
/-- Recurrent formula for `torusIntegral`, see also `torusIntegral_succ`. -/
theorem torusIntegral_succAbove {f : (ℂⁿ ⁺ ¹) → E} {c : ℂⁿ ⁺ ¹} {R : ℝⁿ ⁺ ¹} (hf : TorusIntegrable f c R)
(i : Fin (n + 1)) :
(∯ x in T(c, R), f x) = ∮ x in C(c i, R i), ∯ y in T(c ∘ i.succAbove, R ∘ i.succAbove), f (i.insertNth x y) :=
by
set e : (ℝ × ℝⁿ) ≃ᵐ ℝⁿ ⁺ ¹ := (MeasurableEquiv.piFinSuccAbove (fun _ => ℝ) i).symm
have hem : MeasurePreserving e := (volume_preserving_piFinSuccAbove (fun _ : Fin (n + 1) => ℝ) i).symm _
have heπ : (e ⁻¹' Icc 0 fun _ => 2 * π) = Icc 0 (2 * π) ×ˢ Icc (0 : ℝⁿ) fun _ => 2 * π :=
((Fin.insertNthOrderIso (fun _ => ℝ) i).preimage_Icc _ _).trans (Icc_prod_eq _ _)
rw [torusIntegral, ← hem.map_eq, setIntegral_map_equiv, heπ, Measure.volume_eq_prod, setIntegral_prod,
circleIntegral_def_Icc]
· refine setIntegral_congr_fun measurableSet_Icc fun θ _ => ?_
simp +unfoldPartialApp only [e, torusIntegral, ← integral_smul, deriv_circleMap, i.prod_univ_succAbove _, smul_smul,
torusMap, circleMap_zero]
refine setIntegral_congr_fun measurableSet_Icc fun Θ _ => ?_
simp only [MeasurableEquiv.piFinSuccAbove_symm_apply, i.insertNth_apply_same, i.insertNth_apply_succAbove, (· ∘ ·),
Fin.insertNthEquiv, Equiv.coe_fn_mk]
congr 2
simp only [funext_iff, i.forall_iff_succAbove, circleMap, Fin.insertNth_apply_same, Fin.insertNth_apply_succAbove,
imp_true_iff, and_self_iff]
· have := hf.function_integrable
rwa [← hem.integrableOn_comp_preimage e.measurableEmbedding, heπ] at this
