Theorem: fourierCoeffOn_bound (Carleson/Theorem1_1/Approximation.lean)

State before:
f : ℝ → ℂ
f_continuous : Continuous f
⊢ ∃ C, ∀ (n : ℤ), Complex.abs (fourierCoeffOn Real.two_pi_pos f n) ≤ C
Tactic:
obtain ⟨C, f_bounded⟩ := continuous_bounded f_continuous.continuousOn
State after:
case intro
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
⊢ ∃ C, ∀ (n : ℤ), Complex.abs (fourierCoeffOn Real.two_pi_pos f n) ≤ C

State before:
case intro
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
⊢ ∃ C, ∀ (n : ℤ), Complex.abs (fourierCoeffOn Real.two_pi_pos f n) ≤ C
Tactic:
use C
State after:
case h
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
⊢ ∀ (n : ℤ), Complex.abs (fourierCoeffOn Real.two_pi_pos f n) ≤ C

State before:
case h
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
⊢ ∀ (n : ℤ), Complex.abs (fourierCoeffOn Real.two_pi_pos f n) ≤ C
Tactic:
intro n
State after:
case h
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ Complex.abs (fourierCoeffOn Real.two_pi_pos f n) ≤ C

State before:
case h
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ Complex.abs (fourierCoeffOn Real.two_pi_pos f n) ≤ C
Tactic:
rw [fourierCoeffOn_eq_integral]
State after:
case h
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ Complex.abs ((1 / (2 * Real.pi - 0)) • ∫ (x : ℝ) in 0 ..2 * Real.pi, (fourier (-n)) ↑x • f x) ≤ C

State before:
case h
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ Complex.abs ((1 / (2 * Real.pi - 0)) • ∫ (x : ℝ) in 0 ..2 * Real.pi, (fourier (-n)) ↑x • f x) ≤ C
Tactic:
simp only [sub_zero, one_div, mul_inv_rev, fourier_apply, neg_smul, fourier_neg',
  fourier_coe_apply', Complex.ofReal_mul, Complex.ofReal_ofNat, smul_eq_mul, Complex.real_smul,
  Complex.ofReal_inv, map_mul, map_inv₀, Complex.abs_ofReal, Complex.abs_ofNat]
State after:
case h
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ |Real.pi|⁻¹ * 2⁻¹ *
      Complex.abs
        (∫ (x : ℝ) in 0 ..2 * Real.pi,
          (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (2 * ↑Real.pi)).exp * f x) ≤
    C

State before:
case h
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ |Real.pi|⁻¹ * 2⁻¹ *
      Complex.abs
        (∫ (x : ℝ) in 0 ..2 * Real.pi,
          (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (2 * ↑Real.pi)).exp * f x) ≤
    C
Tactic:
field_simp
State after:
case h
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ Complex.abs
        (∫ (x : ℝ) in 0 ..2 * Real.pi,
          (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (2 * ↑Real.pi)).exp * f x) /
      (|Real.pi| * 2) ≤
    C

State before:
case h
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ Complex.abs
        (∫ (x : ℝ) in 0 ..2 * Real.pi,
          (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (2 * ↑Real.pi)).exp * f x) /
      (|Real.pi| * 2) ≤
    C
Tactic:
rw [abs_of_nonneg Real.pi_pos.le, mul_comm Real.pi, div_le_iff Real.two_pi_pos, ←Complex.norm_eq_abs]
State after:
case h
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ ‖∫ (x : ℝ) in 0 ..2 * Real.pi, (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (2 * ↑Real.pi)).exp * f x‖ ≤
    C * (2 * Real.pi)

State before:
case h
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ ‖∫ (x : ℝ) in 0 ..2 * Real.pi, (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (2 * ↑Real.pi)).exp * f x‖ ≤
    C * (2 * Real.pi)
Tactic:
calc ‖∫ (x : ℝ) in (0 : ℝ)..(2 * Real.pi), (starRingEnd ℂ) (Complex.exp (2 * Real.pi * Complex.I * n * x / (2 * Real.pi))) * f x‖
  _ = ‖∫ (x : ℝ) in (0 : ℝ)..(2 * Real.pi), (starRingEnd ℂ) (Complex.exp (Complex.I * n * x)) * f x‖ := by
    congr
    ext x
    congr
    ring_nf
    rw [mul_comm, ←mul_assoc, ←mul_assoc, ←mul_assoc, inv_mul_cancel]
    . ring
    . simp
      exact Real.pi_pos.ne.symm
  _ ≤ ∫ (x : ℝ) in (0 : ℝ)..(2 * Real.pi), ‖(starRingEnd ℂ) (Complex.exp (Complex.I * n * x)) * f x‖ := by
    apply intervalIntegral.norm_integral_le_integral_norm Real.two_pi_pos.le
  _ = ∫ (x : ℝ) in (0 : ℝ)..(2 * Real.pi), ‖(Complex.exp (Complex.I * n * x)) * f x‖ := by
    simp
  _ = ∫ (x : ℝ) in (0 : ℝ)..(2 * Real.pi), ‖f x‖ := by
    congr
    ext x
    simp only [norm_mul, Complex.norm_eq_abs]
    rw [mul_assoc, mul_comm Complex.I]
    norm_cast
    rw [Complex.abs_exp_ofReal_mul_I]
    ring
  _ ≤ ∫ (_ : ℝ) in (0 : ℝ)..(2 * Real.pi), C := by
    apply intervalIntegral.integral_mono_on
    . exact Real.two_pi_pos.le
    . rw [IntervalIntegrable.intervalIntegrable_norm_iff]
      
      . apply f_continuous.intervalIntegrable
      . apply f_continuous.aestronglyMeasurable
    . apply intervalIntegrable_const
    . intro x hx
      rw [Complex.norm_eq_abs]
      exact f_bounded x hx
  _ = C * (2 * Real.pi) := by
    rw [intervalIntegral.integral_const]
    simp
    ring
State after:
no goals

State before:
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ ‖∫ (x : ℝ) in 0 ..2 * Real.pi, (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (2 * ↑Real.pi)).exp * f x‖ =
    ‖∫ (x : ℝ) in 0 ..2 * Real.pi, (starRingEnd ℂ) (Complex.I * ↑n * ↑x).exp * f x‖
Tactic:
congr
State after:
case e_a.e_f
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ (fun x => (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (2 * ↑Real.pi)).exp * f x) = fun x =>
    (starRingEnd ℂ) (Complex.I * ↑n * ↑x).exp * f x

State before:
case e_a.e_f
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ (fun x => (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (2 * ↑Real.pi)).exp * f x) = fun x =>
    (starRingEnd ℂ) (Complex.I * ↑n * ↑x).exp * f x
Tactic:
ext x
State after:
case e_a.e_f.h
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
x : ℝ
⊢ (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (2 * ↑Real.pi)).exp * f x =
    (starRingEnd ℂ) (Complex.I * ↑n * ↑x).exp * f x

State before:
case e_a.e_f.h
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
x : ℝ
⊢ (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (2 * ↑Real.pi)).exp * f x =
    (starRingEnd ℂ) (Complex.I * ↑n * ↑x).exp * f x
Tactic:
congr
State after:
case e_a.e_f.h.e_a.h.e_6.h.e_z
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
x : ℝ
⊢ 2 * ↑Real.pi * Complex.I * ↑n * ↑x / (2 * ↑Real.pi) = Complex.I * ↑n * ↑x

State before:
case e_a.e_f.h.e_a.h.e_6.h.e_z
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
x : ℝ
⊢ 2 * ↑Real.pi * Complex.I * ↑n * ↑x / (2 * ↑Real.pi) = Complex.I * ↑n * ↑x
Tactic:
ring_nf
State after:
case e_a.e_f.h.e_a.h.e_6.h.e_z
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
x : ℝ
⊢ ↑Real.pi * Complex.I * ↑n * ↑x * (↑Real.pi)⁻¹ = Complex.I * ↑n * ↑x

State before:
case e_a.e_f.h.e_a.h.e_6.h.e_z
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
x : ℝ
⊢ ↑Real.pi * Complex.I * ↑n * ↑x * (↑Real.pi)⁻¹ = Complex.I * ↑n * ↑x
Tactic:
rw [mul_comm, ←mul_assoc, ←mul_assoc, ←mul_assoc, inv_mul_cancel]
State after:
case e_a.e_f.h.e_a.h.e_6.h.e_z
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
x : ℝ
⊢ 1 * Complex.I * ↑n * ↑x = Complex.I * ↑n * ↑x

case e_a.e_f.h.e_a.h.e_6.h.e_z
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
x : ℝ
⊢ ↑Real.pi ≠ 0

State before:
case e_a.e_f.h.e_a.h.e_6.h.e_z
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
x : ℝ
⊢ 1 * Complex.I * ↑n * ↑x = Complex.I * ↑n * ↑x

case e_a.e_f.h.e_a.h.e_6.h.e_z
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
x : ℝ
⊢ ↑Real.pi ≠ 0
Tactic:
. ring
State after:
case e_a.e_f.h.e_a.h.e_6.h.e_z
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
x : ℝ
⊢ ↑Real.pi ≠ 0

State before:
case e_a.e_f.h.e_a.h.e_6.h.e_z
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
x : ℝ
⊢ ↑Real.pi ≠ 0
Tactic:
. simp
  exact Real.pi_pos.ne.symm
State after:
no goals

State before:
case e_a.e_f.h.e_a.h.e_6.h.e_z
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
x : ℝ
⊢ 1 * Complex.I * ↑n * ↑x = Complex.I * ↑n * ↑x
Tactic:
ring
State after:
no goals

State before:
case e_a.e_f.h.e_a.h.e_6.h.e_z
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
x : ℝ
⊢ ↑Real.pi ≠ 0
Tactic:
simp
State after:
case e_a.e_f.h.e_a.h.e_6.h.e_z
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
x : ℝ
⊢ ¬Real.pi = 0

State before:
case e_a.e_f.h.e_a.h.e_6.h.e_z
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
x : ℝ
⊢ ¬Real.pi = 0
Tactic:
exact Real.pi_pos.ne.symm
State after:
no goals

State before:
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ ‖∫ (x : ℝ) in 0 ..2 * Real.pi, (starRingEnd ℂ) (Complex.I * ↑n * ↑x).exp * f x‖ ≤
    ∫ (x : ℝ) in 0 ..2 * Real.pi, ‖(starRingEnd ℂ) (Complex.I * ↑n * ↑x).exp * f x‖
Tactic:
apply intervalIntegral.norm_integral_le_integral_norm Real.two_pi_pos.le
State after:
no goals

State before:
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ ∫ (x : ℝ) in 0 ..2 * Real.pi, ‖(starRingEnd ℂ) (Complex.I * ↑n * ↑x).exp * f x‖ =
    ∫ (x : ℝ) in 0 ..2 * Real.pi, ‖(Complex.I * ↑n * ↑x).exp * f x‖
Tactic:
simp
State after:
no goals

State before:
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ ∫ (x : ℝ) in 0 ..2 * Real.pi, ‖(Complex.I * ↑n * ↑x).exp * f x‖ = ∫ (x : ℝ) in 0 ..2 * Real.pi, ‖f x‖
Tactic:
congr
State after:
case e_f
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ (fun x => ‖(Complex.I * ↑n * ↑x).exp * f x‖) = fun x => ‖f x‖

State before:
case e_f
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ (fun x => ‖(Complex.I * ↑n * ↑x).exp * f x‖) = fun x => ‖f x‖
Tactic:
ext x
State after:
case e_f.h
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
x : ℝ
⊢ ‖(Complex.I * ↑n * ↑x).exp * f x‖ = ‖f x‖

State before:
case e_f.h
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
x : ℝ
⊢ ‖(Complex.I * ↑n * ↑x).exp * f x‖ = ‖f x‖
Tactic:
simp only [norm_mul, Complex.norm_eq_abs]
State after:
case e_f.h
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
x : ℝ
⊢ Complex.abs (Complex.I * ↑n * ↑x).exp * Complex.abs (f x) = Complex.abs (f x)

State before:
case e_f.h
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
x : ℝ
⊢ Complex.abs (Complex.I * ↑n * ↑x).exp * Complex.abs (f x) = Complex.abs (f x)
Tactic:
rw [mul_assoc, mul_comm Complex.I]
State after:
case e_f.h
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
x : ℝ
⊢ Complex.abs (↑n * ↑x * Complex.I).exp * Complex.abs (f x) = Complex.abs (f x)

State before:
case e_f.h
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
x : ℝ
⊢ Complex.abs (↑n * ↑x * Complex.I).exp * Complex.abs (f x) = Complex.abs (f x)
Tactic:
norm_cast
State after:
case e_f.h
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
x : ℝ
⊢ Complex.abs (↑(↑n * x) * Complex.I).exp * Complex.abs (f x) = Complex.abs (f x)

State before:
case e_f.h
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
x : ℝ
⊢ Complex.abs (↑(↑n * x) * Complex.I).exp * Complex.abs (f x) = Complex.abs (f x)
Tactic:
rw [Complex.abs_exp_ofReal_mul_I]
State after:
case e_f.h
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
x : ℝ
⊢ 1 * Complex.abs (f x) = Complex.abs (f x)

State before:
case e_f.h
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
x : ℝ
⊢ 1 * Complex.abs (f x) = Complex.abs (f x)
Tactic:
ring
State after:
no goals

State before:
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ ∫ (x : ℝ) in 0 ..2 * Real.pi, ‖f x‖ ≤ ∫ (x : ℝ) in 0 ..2 * Real.pi, C
Tactic:
apply intervalIntegral.integral_mono_on
State after:
case hab
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ 0 ≤ 2 * Real.pi

case hf
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ IntervalIntegrable (fun u => ‖f u‖) MeasureTheory.volume 0 (2 * Real.pi)

case hg
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ IntervalIntegrable (fun u => C) MeasureTheory.volume 0 (2 * Real.pi)

case h
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ ∀ x ∈ Set.Icc 0 (2 * Real.pi), ‖f x‖ ≤ C

State before:
case hab
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ 0 ≤ 2 * Real.pi

case hf
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ IntervalIntegrable (fun u => ‖f u‖) MeasureTheory.volume 0 (2 * Real.pi)

case hg
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ IntervalIntegrable (fun u => C) MeasureTheory.volume 0 (2 * Real.pi)

case h
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ ∀ x ∈ Set.Icc 0 (2 * Real.pi), ‖f x‖ ≤ C
Tactic:
. exact Real.two_pi_pos.le
State after:
case hf
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ IntervalIntegrable (fun u => ‖f u‖) MeasureTheory.volume 0 (2 * Real.pi)

case hg
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ IntervalIntegrable (fun u => C) MeasureTheory.volume 0 (2 * Real.pi)

case h
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ ∀ x ∈ Set.Icc 0 (2 * Real.pi), ‖f x‖ ≤ C

State before:
case hf
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ IntervalIntegrable (fun u => ‖f u‖) MeasureTheory.volume 0 (2 * Real.pi)

case hg
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ IntervalIntegrable (fun u => C) MeasureTheory.volume 0 (2 * Real.pi)

case h
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ ∀ x ∈ Set.Icc 0 (2 * Real.pi), ‖f x‖ ≤ C
Tactic:
. rw [IntervalIntegrable.intervalIntegrable_norm_iff]
  
  . apply f_continuous.intervalIntegrable
  . apply f_continuous.aestronglyMeasurable
State after:
case hg
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ IntervalIntegrable (fun u => C) MeasureTheory.volume 0 (2 * Real.pi)

case h
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ ∀ x ∈ Set.Icc 0 (2 * Real.pi), ‖f x‖ ≤ C

State before:
case hg
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ IntervalIntegrable (fun u => C) MeasureTheory.volume 0 (2 * Real.pi)

case h
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ ∀ x ∈ Set.Icc 0 (2 * Real.pi), ‖f x‖ ≤ C
Tactic:
. apply intervalIntegrable_const
State after:
case h
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ ∀ x ∈ Set.Icc 0 (2 * Real.pi), ‖f x‖ ≤ C

State before:
case h
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ ∀ x ∈ Set.Icc 0 (2 * Real.pi), ‖f x‖ ≤ C
Tactic:
. intro x hx
  rw [Complex.norm_eq_abs]
  exact f_bounded x hx
State after:
no goals

State before:
case hab
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ 0 ≤ 2 * Real.pi
Tactic:
exact Real.two_pi_pos.le
State after:
no goals

State before:
case hf
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ IntervalIntegrable (fun u => ‖f u‖) MeasureTheory.volume 0 (2 * Real.pi)
Tactic:
rw [IntervalIntegrable.intervalIntegrable_norm_iff]
State after:
case hf
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ IntervalIntegrable (fun u => f u) MeasureTheory.volume 0 (2 * Real.pi)

case hf
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ MeasureTheory.AEStronglyMeasurable (fun u => f u) (MeasureTheory.volume.restrict (Ι 0 (2 * Real.pi)))

State before:
case hf
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ IntervalIntegrable (fun u => f u) MeasureTheory.volume 0 (2 * Real.pi)

case hf
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ MeasureTheory.AEStronglyMeasurable (fun u => f u) (MeasureTheory.volume.restrict (Ι 0 (2 * Real.pi)))
Tactic:
. apply f_continuous.intervalIntegrable
State after:
case hf
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ MeasureTheory.AEStronglyMeasurable (fun u => f u) (MeasureTheory.volume.restrict (Ι 0 (2 * Real.pi)))

State before:
case hf
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ MeasureTheory.AEStronglyMeasurable (fun u => f u) (MeasureTheory.volume.restrict (Ι 0 (2 * Real.pi)))
Tactic:
. apply f_continuous.aestronglyMeasurable
State after:
no goals

State before:
case hf
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ IntervalIntegrable (fun u => f u) MeasureTheory.volume 0 (2 * Real.pi)
Tactic:
apply f_continuous.intervalIntegrable
State after:
no goals

State before:
case hf
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ MeasureTheory.AEStronglyMeasurable (fun u => f u) (MeasureTheory.volume.restrict (Ι 0 (2 * Real.pi)))
Tactic:
apply f_continuous.aestronglyMeasurable
State after:
no goals

State before:
case hg
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ IntervalIntegrable (fun u => C) MeasureTheory.volume 0 (2 * Real.pi)
Tactic:
apply intervalIntegrable_const
State after:
no goals

State before:
case h
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ ∀ x ∈ Set.Icc 0 (2 * Real.pi), ‖f x‖ ≤ C
Tactic:
intro x hx
State after:
case h
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
⊢ ‖f x‖ ≤ C

State before:
case h
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
⊢ ‖f x‖ ≤ C
Tactic:
rw [Complex.norm_eq_abs]
State after:
case h
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
⊢ Complex.abs (f x) ≤ C

State before:
case h
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
⊢ Complex.abs (f x) ≤ C
Tactic:
exact f_bounded x hx
State after:
no goals

State before:
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ ∫ (x : ℝ) in 0 ..2 * Real.pi, C = C * (2 * Real.pi)
Tactic:
rw [intervalIntegral.integral_const]
State after:
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ (2 * Real.pi - 0) • C = C * (2 * Real.pi)

State before:
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ (2 * Real.pi - 0) • C = C * (2 * Real.pi)
Tactic:
simp
State after:
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ 2 * Real.pi * C = C * (2 * Real.pi)

State before:
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ 2 * Real.pi * C = C * (2 * Real.pi)
Tactic:
ring
State after:
no goals