[GOAL]
n : ℕ
E : Type u_1
inst✝ : NormedAddCommGroup E
c : Fin n → ℂ
R θ : Fin n → ℝ
⊢ torusMap c R θ - c = torusMap 0 R θ
[PROOFSTEP]
ext1 i
[GOAL]
case h
n : ℕ
E : Type u_1
inst✝ : NormedAddCommGroup E
c : Fin n → ℂ
R θ : Fin n → ℝ
i : Fin n
⊢ (torusMap c R θ - c) i = torusMap 0 R θ i
[PROOFSTEP]
simp [torusMap]
[GOAL]
n : ℕ
E : Type u_1
inst✝ : NormedAddCommGroup E
c : Fin n → ℂ
R θ : Fin n → ℝ
⊢ torusMap c R θ = c ↔ R = 0
[PROOFSTEP]
simp [funext_iff, torusMap, exp_ne_zero]
[GOAL]
n : ℕ
E : Type u_1
inst✝ : NormedAddCommGroup E
f g : (Fin n → ℂ) → E
c✝ : Fin n → ℂ
R✝ : Fin n → ℝ
a : E
c : Fin n → ℂ
R : Fin n → ℝ
⊢ TorusIntegrable (fun x => a) c R
[PROOFSTEP]
simp [TorusIntegrable, measure_Icc_lt_top]
[GOAL]
n : ℕ
E : Type u_1
inst✝ : NormedAddCommGroup E
f✝ g : (Fin n → ℂ) → E
c✝ : Fin n → ℂ
R : Fin n → ℝ
f : (Fin n → ℂ) → E
c : Fin n → ℂ
⊢ TorusIntegrable f c 0
[PROOFSTEP]
rw [TorusIntegrable, torusMap_zero_radius]
[GOAL]
n : ℕ
E : Type u_1
inst✝ : NormedAddCommGroup E
f✝ g : (Fin n → ℂ) → E
c✝ : Fin n → ℂ
R : Fin n → ℝ
f : (Fin n → ℂ) → E
c : Fin n → ℂ
⊢ IntegrableOn (fun θ => f (const (Fin n → ℝ) c θ)) (Icc 0 fun x => 2 * π)
[PROOFSTEP]
apply torusIntegrable_const (f c) c 0
[GOAL]
n : ℕ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f g : (Fin n → ℂ) → E
c : Fin n → ℂ
R : Fin n → ℝ
inst✝ : NormedSpace ℂ E
hf : TorusIntegrable f c R
⊢ IntegrableOn (fun θ => (∏ i : Fin n, ↑(R i) * exp (↑(θ i) * I) * I) • f (torusMap c R θ)) (Icc 0 fun x => 2 * π)
[PROOFSTEP]
refine' (hf.norm.const_mul (∏ i, |R i|)).mono' _ _
[GOAL]
case refine'_1
n : ℕ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f g : (Fin n → ℂ) → E
c : Fin n → ℂ
R : Fin n → ℝ
inst✝ : NormedSpace ℂ E
hf : TorusIntegrable f c R
⊢ AEStronglyMeasurable (fun θ => (∏ i : Fin n, ↑(R i) * exp (↑(θ i) * I) * I) • f (torusMap c R θ))
    (Measure.restrict volume (Icc 0 fun x => 2 * π))
[PROOFSTEP]
refine (Continuous.aestronglyMeasurable ?_).smul hf.1
[GOAL]
case refine'_1
n : ℕ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f g : (Fin n → ℂ) → E
c : Fin n → ℂ
R : Fin n → ℝ
inst✝ : NormedSpace ℂ E
hf : TorusIntegrable f c R
⊢ Continuous fun θ => ∏ i : Fin n, ↑(R i) * exp (↑(θ i) * I) * I
[PROOFSTEP]
continuity
[GOAL]
case refine'_2
n : ℕ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f g : (Fin n → ℂ) → E
c : Fin n → ℂ
R : Fin n → ℝ
inst✝ : NormedSpace ℂ E
hf : TorusIntegrable f c R
⊢ ∀ᵐ (a : Fin n → ℝ) ∂Measure.restrict volume (Icc 0 fun x => 2 * π),
    ‖(∏ i : Fin n, ↑(R i) * exp (↑(a i) * I) * I) • f (torusMap c R a)‖ ≤ (∏ i : Fin n, |R i|) * ‖f (torusMap c R a)‖
[PROOFSTEP]
simp [norm_smul, map_prod]
[GOAL]
n : ℕ
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ g : (Fin n → ℂ) → E
c✝ : Fin n → ℂ
R : Fin n → ℝ
hn : n ≠ 0
f : (Fin n → ℂ) → E
c : Fin n → ℂ
⊢ (∯ (x : Fin n → ℂ) in T(c, 0), f x) = 0
[PROOFSTEP]
simp only [torusIntegral, Pi.zero_apply, ofReal_zero, mul_zero, zero_mul, Fin.prod_const, zero_pow' n hn, zero_smul,
  integral_zero]
[GOAL]
n : ℕ
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ g : (Fin n → ℂ) → E
c✝ : Fin n → ℂ
R✝ : Fin n → ℝ
f : (Fin n → ℂ) → E
c : Fin n → ℂ
R : Fin n → ℝ
⊢ (∯ (x : Fin n → ℂ) in T(c, R), -f x) = -∯ (x : Fin n → ℂ) in T(c, R), f x
[PROOFSTEP]
simp [torusIntegral, integral_neg]
[GOAL]
n : ℕ
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f g : (Fin n → ℂ) → E
c : Fin n → ℂ
R : Fin n → ℝ
hf : TorusIntegrable f c R
hg : TorusIntegrable g c R
⊢ (∯ (x : Fin n → ℂ) in T(c, R), f x + g x) = (∯ (x : Fin n → ℂ) in T(c, R), f x) + ∯ (x : Fin n → ℂ) in T(c, R), g x
[PROOFSTEP]
simpa only [torusIntegral, smul_add, Pi.add_apply] using integral_add hf.function_integrable hg.function_integrable
[GOAL]
n : ℕ
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f g : (Fin n → ℂ) → E
c : Fin n → ℂ
R : Fin n → ℝ
hf : TorusIntegrable f c R
hg : TorusIntegrable g c R
⊢ (∯ (x : Fin n → ℂ) in T(c, R), f x - g x) = (∯ (x : Fin n → ℂ) in T(c, R), f x) - ∯ (x : Fin n → ℂ) in T(c, R), g x
[PROOFSTEP]
simpa only [sub_eq_add_neg, ← torusIntegral_neg] using torusIntegral_add hf hg.neg
[GOAL]
n : ℕ
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
inst✝³ : CompleteSpace E
f✝ g : (Fin n → ℂ) → E
c✝ : Fin n → ℂ
R✝ : Fin n → ℝ
𝕜 : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : SMulCommClass 𝕜 ℂ E
a : 𝕜
f : (Fin n → ℂ) → E
c : Fin n → ℂ
R : Fin n → ℝ
⊢ (∯ (x : Fin n → ℂ) in T(c, R), a • f x) = a • ∯ (x : Fin n → ℂ) in T(c, R), f x
[PROOFSTEP]
simp only [torusIntegral, integral_smul, ← smul_comm a (_ : ℂ) (_ : E)]
[GOAL]
n : ℕ
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f g : (Fin n → ℂ) → E
c : Fin n → ℂ
R : Fin n → ℝ
C : ℝ
hf : ∀ (θ : Fin n → ℝ), ‖f (torusMap c R θ)‖ ≤ C
θ : Fin n → ℝ
x✝ : θ ∈ Icc 0 fun x => 2 * π
⊢ ‖(∏ i : Fin n, ↑(R i) * exp (↑(θ i) * I) * I) • f (torusMap c R θ)‖ = (∏ i : Fin n, |R i|) * ‖f (torusMap c R θ)‖
[PROOFSTEP]
simp [norm_smul]
[GOAL]
n : ℕ
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f g : (Fin n → ℂ) → E
c : Fin n → ℂ
R : Fin n → ℝ
C : ℝ
hf : ∀ (θ : Fin n → ℝ), ‖f (torusMap c R θ)‖ ≤ C
⊢ (∏ i : Fin n, |R i|) * C * ENNReal.toReal (↑↑volume (Icc 0 fun x => 2 * π)) = ((2 * π) ^ n * ∏ i : Fin n, |R i|) * C
[PROOFSTEP]
simp only [Pi.zero_def, Real.volume_Icc_pi_toReal fun _ => Real.two_pi_pos.le, sub_zero, Fin.prod_const, mul_assoc,
  mul_comm ((2 * π) ^ (n : ℕ))]
[GOAL]
n : ℕ
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ g : (Fin n → ℂ) → E
c✝ : Fin n → ℂ
R✝ : Fin n → ℝ
f : (Fin 0 → ℂ) → E
c : Fin 0 → ℂ
R : Fin 0 → ℝ
⊢ (∯ (x : Fin 0 → ℂ) in T(c, R), f x) = f c
[PROOFSTEP]
simp only [torusIntegral, Fin.prod_univ_zero, one_smul, Subsingleton.elim (fun _ : Fin 0 => 2 * π) 0, Icc_self,
  Measure.restrict_singleton, volume_pi, integral_smul_measure, integral_dirac,
  Measure.pi_of_empty (fun _ : Fin 0 ↦ volume) 0, Measure.dirac_apply_of_mem (mem_singleton _),
  Subsingleton.elim (torusMap c R 0) c]
[GOAL]
n : ℕ
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ g : (Fin n → ℂ) → E
c✝ : Fin n → ℂ
R✝ : Fin n → ℝ
f : (Fin 1 → ℂ) → E
c : Fin 1 → ℂ
R : Fin 1 → ℝ
⊢ (∯ (x : Fin 1 → ℂ) in T(c, R), f x) = ∮ (z : ℂ) in C(c 0, R 0), f fun x => z
[PROOFSTEP]
have H₁ : (((MeasurableEquiv.funUnique _ _).symm) ⁻¹' Icc 0 fun _ => 2 * π) = Icc 0 (2 * π) :=
  (OrderIso.funUnique (Fin 1) ℝ).symm.preimage_Icc _ _
[GOAL]
n : ℕ
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ g : (Fin n → ℂ) → E
c✝ : Fin n → ℂ
R✝ : Fin n → ℝ
f : (Fin 1 → ℂ) → E
c : Fin 1 → ℂ
R : Fin 1 → ℝ
H₁ : (↑(MeasurableEquiv.symm (MeasurableEquiv.funUnique (Fin 1) ℝ)) ⁻¹' Icc 0 fun x => 2 * π) = Icc 0 (2 * π)
⊢ (∯ (x : Fin 1 → ℂ) in T(c, R), f x) = ∮ (z : ℂ) in C(c 0, R 0), f fun x => z
[PROOFSTEP]
have H₂ : torusMap c R = fun θ _ ↦ circleMap (c 0) (R 0) (θ 0) :=
  by
  ext θ i : 2
  rw [Subsingleton.elim i 0]; rfl
[GOAL]
n : ℕ
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ g : (Fin n → ℂ) → E
c✝ : Fin n → ℂ
R✝ : Fin n → ℝ
f : (Fin 1 → ℂ) → E
c : Fin 1 → ℂ
R : Fin 1 → ℝ
H₁ : (↑(MeasurableEquiv.symm (MeasurableEquiv.funUnique (Fin 1) ℝ)) ⁻¹' Icc 0 fun x => 2 * π) = Icc 0 (2 * π)
⊢ torusMap c R = fun θ x => circleMap (c 0) (R 0) (θ 0)
[PROOFSTEP]
ext θ i : 2
[GOAL]
case h.h
n : ℕ
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ g : (Fin n → ℂ) → E
c✝ : Fin n → ℂ
R✝ : Fin n → ℝ
f : (Fin 1 → ℂ) → E
c : Fin 1 → ℂ
R : Fin 1 → ℝ
H₁ : (↑(MeasurableEquiv.symm (MeasurableEquiv.funUnique (Fin 1) ℝ)) ⁻¹' Icc 0 fun x => 2 * π) = Icc 0 (2 * π)
θ : Fin 1 → ℝ
i : Fin 1
⊢ torusMap c R θ i = circleMap (c 0) (R 0) (θ 0)
[PROOFSTEP]
rw [Subsingleton.elim i 0]
[GOAL]
case h.h
n : ℕ
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ g : (Fin n → ℂ) → E
c✝ : Fin n → ℂ
R✝ : Fin n → ℝ
f : (Fin 1 → ℂ) → E
c : Fin 1 → ℂ
R : Fin 1 → ℝ
H₁ : (↑(MeasurableEquiv.symm (MeasurableEquiv.funUnique (Fin 1) ℝ)) ⁻¹' Icc 0 fun x => 2 * π) = Icc 0 (2 * π)
θ : Fin 1 → ℝ
i : Fin 1
⊢ torusMap c R θ 0 = circleMap (c 0) (R 0) (θ 0)
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ g : (Fin n → ℂ) → E
c✝ : Fin n → ℂ
R✝ : Fin n → ℝ
f : (Fin 1 → ℂ) → E
c : Fin 1 → ℂ
R : Fin 1 → ℝ
H₁ : (↑(MeasurableEquiv.symm (MeasurableEquiv.funUnique (Fin 1) ℝ)) ⁻¹' Icc 0 fun x => 2 * π) = Icc 0 (2 * π)
H₂ : torusMap c R = fun θ x => circleMap (c 0) (R 0) (θ 0)
⊢ (∯ (x : Fin 1 → ℂ) in T(c, R), f x) = ∮ (z : ℂ) in C(c 0, R 0), f fun x => z
[PROOFSTEP]
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 _).set_integral_preimage_emb (MeasurableEquiv.measurableEmbedding _),
  H₁, H₂]
[GOAL]
n : ℕ
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ g : (Fin n → ℂ) → E
c✝ : Fin n → ℂ
R✝ : Fin n → ℝ
f : (Fin 1 → ℂ) → E
c : Fin 1 → ℂ
R : Fin 1 → ℝ
H₁ : (↑(MeasurableEquiv.symm (MeasurableEquiv.funUnique (Fin 1) ℝ)) ⁻¹' Icc 0 fun x => 2 * π) = Icc 0 (2 * π)
H₂ : torusMap c R = fun θ x => circleMap (c 0) (R 0) (θ 0)
⊢ ∫ (x : ℝ) in Icc 0 (2 * π),
      (∏ i : Fin 1, ↑(R i) * exp (↑(↑(MeasurableEquiv.symm (MeasurableEquiv.funUnique (Fin 1) ℝ)) x i) * I) * I) •
        f ((fun θ x => circleMap (c 0) (R 0) (θ 0)) (↑(MeasurableEquiv.symm (MeasurableEquiv.funUnique (Fin 1) ℝ)) x)) =
    ∫ (x : ℝ) in Icc 0 (2 * π), deriv (circleMap (c 0) (R 0)) x • f fun x_1 => circleMap (c 0) (R 0) x
[PROOFSTEP]
simp [circleMap_zero]
[GOAL]
n : ℕ
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ g : (Fin n → ℂ) → E
c✝ : Fin n → ℂ
R✝ : Fin n → ℝ
f : (Fin (n + 1) → ℂ) → E
c : Fin (n + 1) → ℂ
R : Fin (n + 1) → ℝ
hf : TorusIntegrable f c R
i : Fin (n + 1)
⊢ (∯ (x : Fin (n + 1) → ℂ) in T(c, R), f x) =
    ∮ (x : ℂ) in C(c i, R i), ∯ (y : Fin n → ℂ) in T(c ∘ Fin.succAbove i, R ∘ Fin.succAbove i), f (Fin.insertNth i x y)
[PROOFSTEP]
set e : ℝ × ℝⁿ ≃ᵐ ℝⁿ⁺¹ := (MeasurableEquiv.piFinSuccAboveEquiv (fun _ => ℝ) i).symm
[GOAL]
n : ℕ
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ g : (Fin n → ℂ) → E
c✝ : Fin n → ℂ
R✝ : Fin n → ℝ
f : (Fin (n + 1) → ℂ) → E
c : Fin (n + 1) → ℂ
R : Fin (n + 1) → ℝ
hf : TorusIntegrable f c R
i : Fin (n + 1)
e : ℝ × (Fin n → ℝ) ≃ᵐ (Fin (n + 1) → ℝ) := MeasurableEquiv.symm (MeasurableEquiv.piFinSuccAboveEquiv (fun x => ℝ) i)
⊢ (∯ (x : Fin (n + 1) → ℂ) in T(c, R), f x) =
    ∮ (x : ℂ) in C(c i, R i), ∯ (y : Fin n → ℂ) in T(c ∘ Fin.succAbove i, R ∘ Fin.succAbove i), f (Fin.insertNth i x y)
[PROOFSTEP]
have hem : MeasurePreserving e := (volume_preserving_piFinSuccAboveEquiv (fun _ : Fin (n + 1) => ℝ) i).symm _
[GOAL]
n : ℕ
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ g : (Fin n → ℂ) → E
c✝ : Fin n → ℂ
R✝ : Fin n → ℝ
f : (Fin (n + 1) → ℂ) → E
c : Fin (n + 1) → ℂ
R : Fin (n + 1) → ℝ
hf : TorusIntegrable f c R
i : Fin (n + 1)
e : ℝ × (Fin n → ℝ) ≃ᵐ (Fin (n + 1) → ℝ) := MeasurableEquiv.symm (MeasurableEquiv.piFinSuccAboveEquiv (fun x => ℝ) i)
hem : MeasurePreserving ↑e
⊢ (∯ (x : Fin (n + 1) → ℂ) in T(c, R), f x) =
    ∮ (x : ℂ) in C(c i, R i), ∯ (y : Fin n → ℂ) in T(c ∘ Fin.succAbove i, R ∘ Fin.succAbove i), f (Fin.insertNth i x y)
[PROOFSTEP]
have heπ : (e ⁻¹' Icc 0 fun _ => 2 * π) = Icc 0 (2 * π) ×ˢ Icc (0 : ℝⁿ) fun _ => 2 * π :=
  ((OrderIso.piFinSuccAboveIso (fun _ => ℝ) i).symm.preimage_Icc _ _).trans (Icc_prod_eq _ _)
[GOAL]
n : ℕ
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ g : (Fin n → ℂ) → E
c✝ : Fin n → ℂ
R✝ : Fin n → ℝ
f : (Fin (n + 1) → ℂ) → E
c : Fin (n + 1) → ℂ
R : Fin (n + 1) → ℝ
hf : TorusIntegrable f c R
i : Fin (n + 1)
e : ℝ × (Fin n → ℝ) ≃ᵐ (Fin (n + 1) → ℝ) := MeasurableEquiv.symm (MeasurableEquiv.piFinSuccAboveEquiv (fun x => ℝ) i)
hem : MeasurePreserving ↑e
heπ : (↑e ⁻¹' Icc 0 fun x => 2 * π) = Icc 0 (2 * π) ×ˢ Icc 0 fun x => 2 * π
⊢ (∯ (x : Fin (n + 1) → ℂ) in T(c, R), f x) =
    ∮ (x : ℂ) in C(c i, R i), ∯ (y : Fin n → ℂ) in T(c ∘ Fin.succAbove i, R ∘ Fin.succAbove i), f (Fin.insertNth i x y)
[PROOFSTEP]
rw [torusIntegral, ← hem.map_eq, set_integral_map_equiv, heπ, Measure.volume_eq_prod, set_integral_prod,
  circleIntegral_def_Icc]
[GOAL]
n : ℕ
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ g : (Fin n → ℂ) → E
c✝ : Fin n → ℂ
R✝ : Fin n → ℝ
f : (Fin (n + 1) → ℂ) → E
c : Fin (n + 1) → ℂ
R : Fin (n + 1) → ℝ
hf : TorusIntegrable f c R
i : Fin (n + 1)
e : ℝ × (Fin n → ℝ) ≃ᵐ (Fin (n + 1) → ℝ) := MeasurableEquiv.symm (MeasurableEquiv.piFinSuccAboveEquiv (fun x => ℝ) i)
hem : MeasurePreserving ↑e
heπ : (↑e ⁻¹' Icc 0 fun x => 2 * π) = Icc 0 (2 * π) ×ˢ Icc 0 fun x => 2 * π
⊢ ∫ (x : ℝ) in Icc 0 (2 * π),
      ∫ (y : Fin n → ℝ) in Icc 0 fun x => 2 * π,
        (∏ i : Fin (n + 1), ↑(R i) * exp (↑(↑e (x, y) i) * I) * I) • f (torusMap c R (↑e (x, y))) =
    ∫ (θ : ℝ) in Icc 0 (2 * π),
      deriv (circleMap (c i) (R i)) θ •
        ∯ (y : Fin n → ℂ) in T(c ∘ Fin.succAbove i, R ∘ Fin.succAbove i),
          f (Fin.insertNth i (circleMap (c i) (R i) θ) y)
[PROOFSTEP]
refine' set_integral_congr measurableSet_Icc fun θ _ => _
[GOAL]
n : ℕ
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ g : (Fin n → ℂ) → E
c✝ : Fin n → ℂ
R✝ : Fin n → ℝ
f : (Fin (n + 1) → ℂ) → E
c : Fin (n + 1) → ℂ
R : Fin (n + 1) → ℝ
hf : TorusIntegrable f c R
i : Fin (n + 1)
e : ℝ × (Fin n → ℝ) ≃ᵐ (Fin (n + 1) → ℝ) := MeasurableEquiv.symm (MeasurableEquiv.piFinSuccAboveEquiv (fun x => ℝ) i)
hem : MeasurePreserving ↑e
heπ : (↑e ⁻¹' Icc 0 fun x => 2 * π) = Icc 0 (2 * π) ×ˢ Icc 0 fun x => 2 * π
θ : ℝ
x✝ : θ ∈ Icc 0 (2 * π)
⊢ ∫ (y : Fin n → ℝ) in Icc 0 fun x => 2 * π,
      (∏ i : Fin (n + 1), ↑(R i) * exp (↑(↑e (θ, y) i) * I) * I) • f (torusMap c R (↑e (θ, y))) =
    deriv (circleMap (c i) (R i)) θ •
      ∯ (y : Fin n → ℂ) in T(c ∘ Fin.succAbove i, R ∘ Fin.succAbove i), f (Fin.insertNth i (circleMap (c i) (R i) θ) y)
[PROOFSTEP]
simp only [torusIntegral, ← integral_smul, deriv_circleMap, i.prod_univ_succAbove _, smul_smul, torusMap,
  circleMap_zero]
[GOAL]
n : ℕ
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ g : (Fin n → ℂ) → E
c✝ : Fin n → ℂ
R✝ : Fin n → ℝ
f : (Fin (n + 1) → ℂ) → E
c : Fin (n + 1) → ℂ
R : Fin (n + 1) → ℝ
hf : TorusIntegrable f c R
i : Fin (n + 1)
e : ℝ × (Fin n → ℝ) ≃ᵐ (Fin (n + 1) → ℝ) := MeasurableEquiv.symm (MeasurableEquiv.piFinSuccAboveEquiv (fun x => ℝ) i)
hem : MeasurePreserving ↑e
heπ : (↑e ⁻¹' Icc 0 fun x => 2 * π) = Icc 0 (2 * π) ×ˢ Icc 0 fun x => 2 * π
θ : ℝ
x✝ : θ ∈ Icc 0 (2 * π)
⊢ (∫ (y : Fin n → ℝ) in Icc 0 fun x => 2 * π,
      (↑(R i) * exp (↑(↑(MeasurableEquiv.symm (MeasurableEquiv.piFinSuccAboveEquiv (fun x => ℝ) i)) (θ, y) i) * I) * I *
          ∏ i_1 : Fin n,
            ↑(R (Fin.succAbove i i_1)) *
                exp
                  (↑(↑(MeasurableEquiv.symm (MeasurableEquiv.piFinSuccAboveEquiv (fun x => ℝ) i)) (θ, y)
                        (Fin.succAbove i i_1)) *
                    I) *
              I) •
        f fun i_1 =>
          c i_1 +
            ↑(R i_1) *
              exp (↑(↑(MeasurableEquiv.symm (MeasurableEquiv.piFinSuccAboveEquiv (fun x => ℝ) i)) (θ, y) i_1) * I)) =
    ∫ (a : Fin n → ℝ) in Icc 0 fun x => 2 * π,
      (↑(R i) * exp (↑θ * I) * I * ∏ i_1 : Fin n, ↑((R ∘ Fin.succAbove i) i_1) * exp (↑(a i_1) * I) * I) •
        f
          (Fin.insertNth i (circleMap (c i) (R i) θ) fun i_1 =>
            (c ∘ Fin.succAbove i) i_1 + ↑((R ∘ Fin.succAbove i) i_1) * exp (↑(a i_1) * I))
[PROOFSTEP]
refine' set_integral_congr measurableSet_Icc fun Θ _ => _
[GOAL]
n : ℕ
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ g : (Fin n → ℂ) → E
c✝ : Fin n → ℂ
R✝ : Fin n → ℝ
f : (Fin (n + 1) → ℂ) → E
c : Fin (n + 1) → ℂ
R : Fin (n + 1) → ℝ
hf : TorusIntegrable f c R
i : Fin (n + 1)
e : ℝ × (Fin n → ℝ) ≃ᵐ (Fin (n + 1) → ℝ) := MeasurableEquiv.symm (MeasurableEquiv.piFinSuccAboveEquiv (fun x => ℝ) i)
hem : MeasurePreserving ↑e
heπ : (↑e ⁻¹' Icc 0 fun x => 2 * π) = Icc 0 (2 * π) ×ˢ Icc 0 fun x => 2 * π
θ : ℝ
x✝¹ : θ ∈ Icc 0 (2 * π)
Θ : Fin n → ℝ
x✝ : Θ ∈ Icc 0 fun x => 2 * π
⊢ ((↑(R i) * exp (↑(↑(MeasurableEquiv.symm (MeasurableEquiv.piFinSuccAboveEquiv (fun x => ℝ) i)) (θ, Θ) i) * I) * I *
        ∏ i_1 : Fin n,
          ↑(R (Fin.succAbove i i_1)) *
              exp
                (↑(↑(MeasurableEquiv.symm (MeasurableEquiv.piFinSuccAboveEquiv (fun x => ℝ) i)) (θ, Θ)
                      (Fin.succAbove i i_1)) *
                  I) *
            I) •
      f fun i_1 =>
        c i_1 +
          ↑(R i_1) *
            exp (↑(↑(MeasurableEquiv.symm (MeasurableEquiv.piFinSuccAboveEquiv (fun x => ℝ) i)) (θ, Θ) i_1) * I)) =
    (↑(R i) * exp (↑θ * I) * I * ∏ i_1 : Fin n, ↑((R ∘ Fin.succAbove i) i_1) * exp (↑(Θ i_1) * I) * I) •
      f
        (Fin.insertNth i (circleMap (c i) (R i) θ) fun i_1 =>
          (c ∘ Fin.succAbove i) i_1 + ↑((R ∘ Fin.succAbove i) i_1) * exp (↑(Θ i_1) * I))
[PROOFSTEP]
simp only [MeasurableEquiv.piFinSuccAboveEquiv_symm_apply, i.insertNth_apply_same, i.insertNth_apply_succAbove, (· ∘ ·)]
[GOAL]
n : ℕ
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ g : (Fin n → ℂ) → E
c✝ : Fin n → ℂ
R✝ : Fin n → ℝ
f : (Fin (n + 1) → ℂ) → E
c : Fin (n + 1) → ℂ
R : Fin (n + 1) → ℝ
hf : TorusIntegrable f c R
i : Fin (n + 1)
e : ℝ × (Fin n → ℝ) ≃ᵐ (Fin (n + 1) → ℝ) := MeasurableEquiv.symm (MeasurableEquiv.piFinSuccAboveEquiv (fun x => ℝ) i)
hem : MeasurePreserving ↑e
heπ : (↑e ⁻¹' Icc 0 fun x => 2 * π) = Icc 0 (2 * π) ×ˢ Icc 0 fun x => 2 * π
θ : ℝ
x✝¹ : θ ∈ Icc 0 (2 * π)
Θ : Fin n → ℝ
x✝ : Θ ∈ Icc 0 fun x => 2 * π
⊢ ((↑(R i) * exp (↑θ * I) * I * ∏ x : Fin n, ↑(R (Fin.succAbove i x)) * exp (↑(Θ x) * I) * I) •
      f fun i_1 => c i_1 + ↑(R i_1) * exp (↑(Fin.insertNth i θ Θ i_1) * I)) =
    (↑(R i) * exp (↑θ * I) * I * ∏ x : Fin n, ↑(R (Fin.succAbove i x)) * exp (↑(Θ x) * I) * I) •
      f
        (Fin.insertNth i (circleMap (c i) (R i) θ) fun i_1 =>
          c (Fin.succAbove i i_1) + ↑(R (Fin.succAbove i i_1)) * exp (↑(Θ i_1) * I))
[PROOFSTEP]
congr 2
[GOAL]
case e_a.e_a
n : ℕ
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ g : (Fin n → ℂ) → E
c✝ : Fin n → ℂ
R✝ : Fin n → ℝ
f : (Fin (n + 1) → ℂ) → E
c : Fin (n + 1) → ℂ
R : Fin (n + 1) → ℝ
hf : TorusIntegrable f c R
i : Fin (n + 1)
e : ℝ × (Fin n → ℝ) ≃ᵐ (Fin (n + 1) → ℝ) := MeasurableEquiv.symm (MeasurableEquiv.piFinSuccAboveEquiv (fun x => ℝ) i)
hem : MeasurePreserving ↑e
heπ : (↑e ⁻¹' Icc 0 fun x => 2 * π) = Icc 0 (2 * π) ×ˢ Icc 0 fun x => 2 * π
θ : ℝ
x✝¹ : θ ∈ Icc 0 (2 * π)
Θ : Fin n → ℝ
x✝ : Θ ∈ Icc 0 fun x => 2 * π
⊢ (fun i_1 => c i_1 + ↑(R i_1) * exp (↑(Fin.insertNth i θ Θ i_1) * I)) =
    Fin.insertNth i (circleMap (c i) (R i) θ) fun i_1 =>
      c (Fin.succAbove i i_1) + ↑(R (Fin.succAbove i i_1)) * exp (↑(Θ i_1) * I)
[PROOFSTEP]
simp only [funext_iff, i.forall_iff_succAbove, circleMap, Fin.insertNth_apply_same, eq_self_iff_true,
  Fin.insertNth_apply_succAbove, imp_true_iff, and_self_iff]
[GOAL]
case hf
n : ℕ
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ g : (Fin n → ℂ) → E
c✝ : Fin n → ℂ
R✝ : Fin n → ℝ
f : (Fin (n + 1) → ℂ) → E
c : Fin (n + 1) → ℂ
R : Fin (n + 1) → ℝ
hf : TorusIntegrable f c R
i : Fin (n + 1)
e : ℝ × (Fin n → ℝ) ≃ᵐ (Fin (n + 1) → ℝ) := MeasurableEquiv.symm (MeasurableEquiv.piFinSuccAboveEquiv (fun x => ℝ) i)
hem : MeasurePreserving ↑e
heπ : (↑e ⁻¹' Icc 0 fun x => 2 * π) = Icc 0 (2 * π) ×ˢ Icc 0 fun x => 2 * π
⊢ IntegrableOn (fun x => (∏ i : Fin (n + 1), ↑(R i) * exp (↑(↑e x i) * I) * I) • f (torusMap c R (↑e x)))
    (Icc 0 (2 * π) ×ˢ Icc 0 fun x => 2 * π)
[PROOFSTEP]
have := hf.function_integrable
[GOAL]
case hf
n : ℕ
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ g : (Fin n → ℂ) → E
c✝ : Fin n → ℂ
R✝ : Fin n → ℝ
f : (Fin (n + 1) → ℂ) → E
c : Fin (n + 1) → ℂ
R : Fin (n + 1) → ℝ
hf : TorusIntegrable f c R
i : Fin (n + 1)
e : ℝ × (Fin n → ℝ) ≃ᵐ (Fin (n + 1) → ℝ) := MeasurableEquiv.symm (MeasurableEquiv.piFinSuccAboveEquiv (fun x => ℝ) i)
hem : MeasurePreserving ↑e
heπ : (↑e ⁻¹' Icc 0 fun x => 2 * π) = Icc 0 (2 * π) ×ˢ Icc 0 fun x => 2 * π
this :
  IntegrableOn (fun θ => (∏ i : Fin (n + 1), ↑(R i) * exp (↑(θ i) * I) * I) • f (torusMap c R θ)) (Icc 0 fun x => 2 * π)
⊢ IntegrableOn (fun x => (∏ i : Fin (n + 1), ↑(R i) * exp (↑(↑e x i) * I) * I) • f (torusMap c R (↑e x)))
    (Icc 0 (2 * π) ×ˢ Icc 0 fun x => 2 * π)
[PROOFSTEP]
rwa [← hem.integrableOn_comp_preimage e.measurableEmbedding, heπ] at this 
[GOAL]
n : ℕ
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ g : (Fin n → ℂ) → E
c✝ : Fin n → ℂ
R✝ : Fin n → ℝ
f : (Fin (n + 1) → ℂ) → E
c : Fin (n + 1) → ℂ
R : Fin (n + 1) → ℝ
hf : TorusIntegrable f c R
⊢ (∯ (x : Fin (n + 1) → ℂ) in T(c, R), f x) =
    ∮ (x : ℂ) in C(c 0, R 0), ∯ (y : Fin n → ℂ) in T(c ∘ Fin.succ, R ∘ Fin.succ), f (Fin.cons x y)
[PROOFSTEP]
simpa using torusIntegral_succAbove hf 0
