[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : TopologicalSpace.SecondCountableTopology E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g : α → E
⊢ AEMeasurable g ↔ AEMeasurable fun x => ↑(f x) • g x
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : TopologicalSpace.SecondCountableTopology E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g : α → E
⊢ AEMeasurable g → AEMeasurable fun x => ↑(f x) • g x
[PROOFSTEP]
rintro ⟨g', g'meas, hg'⟩
[GOAL]
case mp.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : TopologicalSpace.SecondCountableTopology E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : Measurable g'
hg' : g =ᵐ[Measure.withDensity μ fun x => ↑(f x)] g'
⊢ AEMeasurable fun x => ↑(f x) • g x
[PROOFSTEP]
have A : MeasurableSet {x : α | f x ≠ 0} := (hf (measurableSet_singleton 0)).compl
[GOAL]
case mp.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : TopologicalSpace.SecondCountableTopology E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : Measurable g'
hg' : g =ᵐ[Measure.withDensity μ fun x => ↑(f x)] g'
A : MeasurableSet {x | f x ≠ 0}
⊢ AEMeasurable fun x => ↑(f x) • g x
[PROOFSTEP]
refine' ⟨fun x => (f x : ℝ) • g' x, hf.coe_nnreal_real.smul g'meas, _⟩
[GOAL]
case mp.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : TopologicalSpace.SecondCountableTopology E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : Measurable g'
hg' : g =ᵐ[Measure.withDensity μ fun x => ↑(f x)] g'
A : MeasurableSet {x | f x ≠ 0}
⊢ (fun x => ↑(f x) • g x) =ᵐ[μ] fun x => ↑(f x) • g' x
[PROOFSTEP]
apply @ae_of_ae_restrict_of_ae_restrict_compl _ _ _ {x | f x ≠ 0}
[GOAL]
case mp.intro.intro.ht
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : TopologicalSpace.SecondCountableTopology E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : Measurable g'
hg' : g =ᵐ[Measure.withDensity μ fun x => ↑(f x)] g'
A : MeasurableSet {x | f x ≠ 0}
⊢ ∀ᵐ (x : α) ∂Measure.restrict μ {x | f x ≠ 0}, (fun x => ↑(f x) • g x) x = (fun x => ↑(f x) • g' x) x
[PROOFSTEP]
rw [EventuallyEq, ae_withDensity_iff hf.coe_nnreal_ennreal] at hg'
[GOAL]
case mp.intro.intro.ht
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : TopologicalSpace.SecondCountableTopology E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : Measurable g'
hg' : ∀ᵐ (x : α) ∂μ, ↑(f x) ≠ 0 → g x = g' x
A : MeasurableSet {x | f x ≠ 0}
⊢ ∀ᵐ (x : α) ∂Measure.restrict μ {x | f x ≠ 0}, (fun x => ↑(f x) • g x) x = (fun x => ↑(f x) • g' x) x
[PROOFSTEP]
rw [ae_restrict_iff' A]
[GOAL]
case mp.intro.intro.ht
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : TopologicalSpace.SecondCountableTopology E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : Measurable g'
hg' : ∀ᵐ (x : α) ∂μ, ↑(f x) ≠ 0 → g x = g' x
A : MeasurableSet {x | f x ≠ 0}
⊢ ∀ᵐ (x : α) ∂μ, x ∈ {x | f x ≠ 0} → (fun x => ↑(f x) • g x) x = (fun x => ↑(f x) • g' x) x
[PROOFSTEP]
filter_upwards [hg']
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : TopologicalSpace.SecondCountableTopology E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : Measurable g'
hg' : ∀ᵐ (x : α) ∂μ, ↑(f x) ≠ 0 → g x = g' x
A : MeasurableSet {x | f x ≠ 0}
⊢ ∀ (a : α), (↑(f a) ≠ 0 → g a = g' a) → f a ≠ 0 → ↑(f a) • g a = ↑(f a) • g' a
[PROOFSTEP]
intro a ha h'a
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : TopologicalSpace.SecondCountableTopology E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : Measurable g'
hg' : ∀ᵐ (x : α) ∂μ, ↑(f x) ≠ 0 → g x = g' x
A : MeasurableSet {x | f x ≠ 0}
a : α
ha : ↑(f a) ≠ 0 → g a = g' a
h'a : f a ≠ 0
⊢ ↑(f a) • g a = ↑(f a) • g' a
[PROOFSTEP]
have : (f a : ℝ≥0∞) ≠ 0 := by simpa only [Ne.def, coe_eq_zero] using h'a
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : TopologicalSpace.SecondCountableTopology E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : Measurable g'
hg' : ∀ᵐ (x : α) ∂μ, ↑(f x) ≠ 0 → g x = g' x
A : MeasurableSet {x | f x ≠ 0}
a : α
ha : ↑(f a) ≠ 0 → g a = g' a
h'a : f a ≠ 0
⊢ ↑(f a) ≠ 0
[PROOFSTEP]
simpa only [Ne.def, coe_eq_zero] using h'a
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : TopologicalSpace.SecondCountableTopology E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : Measurable g'
hg' : ∀ᵐ (x : α) ∂μ, ↑(f x) ≠ 0 → g x = g' x
A : MeasurableSet {x | f x ≠ 0}
a : α
ha : ↑(f a) ≠ 0 → g a = g' a
h'a : f a ≠ 0
this : ↑(f a) ≠ 0
⊢ ↑(f a) • g a = ↑(f a) • g' a
[PROOFSTEP]
rw [ha this]
[GOAL]
case mp.intro.intro.htc
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : TopologicalSpace.SecondCountableTopology E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : Measurable g'
hg' : g =ᵐ[Measure.withDensity μ fun x => ↑(f x)] g'
A : MeasurableSet {x | f x ≠ 0}
⊢ ∀ᵐ (x : α) ∂Measure.restrict μ {x | f x ≠ 0}ᶜ, (fun x => ↑(f x) • g x) x = (fun x => ↑(f x) • g' x) x
[PROOFSTEP]
filter_upwards [ae_restrict_mem A.compl]
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : TopologicalSpace.SecondCountableTopology E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : Measurable g'
hg' : g =ᵐ[Measure.withDensity μ fun x => ↑(f x)] g'
A : MeasurableSet {x | f x ≠ 0}
⊢ ∀ (a : α), a ∈ {x | f x ≠ 0}ᶜ → ↑(f a) • g a = ↑(f a) • g' a
[PROOFSTEP]
intro x hx
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : TopologicalSpace.SecondCountableTopology E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : Measurable g'
hg' : g =ᵐ[Measure.withDensity μ fun x => ↑(f x)] g'
A : MeasurableSet {x | f x ≠ 0}
x : α
hx : x ∈ {x | f x ≠ 0}ᶜ
⊢ ↑(f x) • g x = ↑(f x) • g' x
[PROOFSTEP]
simp only [Classical.not_not, mem_setOf_eq, mem_compl_iff] at hx
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : TopologicalSpace.SecondCountableTopology E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : Measurable g'
hg' : g =ᵐ[Measure.withDensity μ fun x => ↑(f x)] g'
A : MeasurableSet {x | f x ≠ 0}
x : α
hx : f x = 0
⊢ ↑(f x) • g x = ↑(f x) • g' x
[PROOFSTEP]
simp [hx]
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : TopologicalSpace.SecondCountableTopology E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g : α → E
⊢ (AEMeasurable fun x => ↑(f x) • g x) → AEMeasurable g
[PROOFSTEP]
rintro ⟨g', g'meas, hg'⟩
[GOAL]
case mpr.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : TopologicalSpace.SecondCountableTopology E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : Measurable g'
hg' : (fun x => ↑(f x) • g x) =ᵐ[μ] g'
⊢ AEMeasurable g
[PROOFSTEP]
refine' ⟨fun x => (f x : ℝ)⁻¹ • g' x, hf.coe_nnreal_real.inv.smul g'meas, _⟩
[GOAL]
case mpr.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : TopologicalSpace.SecondCountableTopology E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : Measurable g'
hg' : (fun x => ↑(f x) • g x) =ᵐ[μ] g'
⊢ g =ᵐ[Measure.withDensity μ fun x => ↑(f x)] fun x => (↑(f x))⁻¹ • g' x
[PROOFSTEP]
rw [EventuallyEq, ae_withDensity_iff hf.coe_nnreal_ennreal]
[GOAL]
case mpr.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : TopologicalSpace.SecondCountableTopology E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : Measurable g'
hg' : (fun x => ↑(f x) • g x) =ᵐ[μ] g'
⊢ ∀ᵐ (x : α) ∂μ, ↑(f x) ≠ 0 → g x = (↑(f x))⁻¹ • g' x
[PROOFSTEP]
filter_upwards [hg']
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : TopologicalSpace.SecondCountableTopology E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : Measurable g'
hg' : (fun x => ↑(f x) • g x) =ᵐ[μ] g'
⊢ ∀ (a : α), ↑(f a) • g a = g' a → ↑(f a) ≠ 0 → g a = (↑(f a))⁻¹ • g' a
[PROOFSTEP]
intro x hx h'x
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : TopologicalSpace.SecondCountableTopology E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : Measurable g'
hg' : (fun x => ↑(f x) • g x) =ᵐ[μ] g'
x : α
hx : ↑(f x) • g x = g' x
h'x : ↑(f x) ≠ 0
⊢ g x = (↑(f x))⁻¹ • g' x
[PROOFSTEP]
rw [← hx, smul_smul, _root_.inv_mul_cancel, one_smul]
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : TopologicalSpace.SecondCountableTopology E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : Measurable g'
hg' : (fun x => ↑(f x) • g x) =ᵐ[μ] g'
x : α
hx : ↑(f x) • g x = g' x
h'x : ↑(f x) ≠ 0
⊢ ↑(f x) ≠ 0
[PROOFSTEP]
simp only [Ne.def, coe_eq_zero] at h'x
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : TopologicalSpace.SecondCountableTopology E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : Measurable g'
hg' : (fun x => ↑(f x) • g x) =ᵐ[μ] g'
x : α
hx : ↑(f x) • g x = g' x
h'x : ¬f x = 0
⊢ ↑(f x) ≠ 0
[PROOFSTEP]
simpa only [NNReal.coe_eq_zero, Ne.def] using h'x


[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


[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
a b : ℝ
⊢ ⨍ (x : ℝ) in a..b, f x = ⨍ (x : ℝ) in b..a, f x
[PROOFSTEP]
rw [setAverage_eq, setAverage_eq, uIoc_comm]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
a b : ℝ
⊢ ⨍ (x : ℝ) in a..b, f x = (b - a)⁻¹ • ∫ (x : ℝ) in a..b, f x
[PROOFSTEP]
cases' le_or_lt a b with h h
[GOAL]
case inl
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
a b : ℝ
h : a ≤ b
⊢ ⨍ (x : ℝ) in a..b, f x = (b - a)⁻¹ • ∫ (x : ℝ) in a..b, f x
[PROOFSTEP]
rw [setAverage_eq, uIoc_of_le h, Real.volume_Ioc, intervalIntegral.integral_of_le h,
  ENNReal.toReal_ofReal (sub_nonneg.2 h)]
[GOAL]
case inr
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
a b : ℝ
h : b < a
⊢ ⨍ (x : ℝ) in a..b, f x = (b - a)⁻¹ • ∫ (x : ℝ) in a..b, f x
[PROOFSTEP]
rw [setAverage_eq, uIoc_of_lt h, Real.volume_Ioc, intervalIntegral.integral_of_ge h.le,
  ENNReal.toReal_ofReal (sub_nonneg.2 h.le), smul_neg, ← neg_smul, ← inv_neg, neg_sub]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → ℝ
a b : ℝ
⊢ ⨍ (x : ℝ) in a..b, f x = (∫ (x : ℝ) in a..b, f x) / (b - a)
[PROOFSTEP]
rw [interval_average_eq, smul_eq_mul, div_eq_inv_mul]