internlm/Lean-Github huggingface dataset:
Theorem: summable_of_le_on_nonzero
Proof state before:
f g : ℤ → ℝ
hgpos : 0 ≤ g
hgf : ∀ (i : ℤ), i ≠ 0 → g i ≤ f i
summablef : Summable f
f' : ℤ → ℝ := fun i => if i = 0 then g i else f i
f'def : f' = fun i => if i = 0 then g i else f i
this : ∀ (i : ℤ), g i ≤ f' i
s : Finset ℤ := {0}
⊢ ∀ (b : { x // x ∉ s }), f' ↑b = f ↑b
Tactic:
intro ⟨b, hb⟩
Proof state after:
f g : ℤ → ℝ
hgpos : 0 ≤ g
hgf : ∀ (i : ℤ), i ≠ 0 → g i ≤ f i
summablef : Summable f
f' : ℤ → ℝ := fun i => if i = 0 then g i else f i
f'def : f' = fun i => if i = 0 then g i else f i
this : ∀ (i : ℤ), g i ≤ f' i
s : Finset ℤ := {0}
b : ℤ
hb : b ∉ s
⊢ f' ↑⟨b, hb⟩ = f ↑⟨b, hb⟩
Theorem: summable_of_le_on_nonzero
Proof state before:
f g : ℤ → ℝ
hgpos : 0 ≤ g
hgf : ∀ (i : ℤ), i ≠ 0 → g i ≤ f i
summablef : Summable f
f' : ℤ → ℝ := fun i => if i = 0 then g i else f i
f'def : f' = fun i => if i = 0 then g i else f i
this : ∀ (i : ℤ), g i ≤ f' i
s : Finset ℤ := {0}
b : ℤ
hb : b ∉ s
⊢ f' ↑⟨b, hb⟩ = f ↑⟨b, hb⟩
Tactic:
simp
Proof state after:
f g : ℤ → ℝ
hgpos : 0 ≤ g
hgf : ∀ (i : ℤ), i ≠ 0 → g i ≤ f i
summablef : Summable f
f' : ℤ → ℝ := fun i => if i = 0 then g i else f i
f'def : f' = fun i => if i = 0 then g i else f i
this : ∀ (i : ℤ), g i ≤ f' i
s : Finset ℤ := {0}
b : ℤ
hb : b ∉ s
⊢ f' b = f b
Theorem: summable_of_le_on_nonzero
Proof state before:
f g : ℤ → ℝ
hgpos : 0 ≤ g
hgf : ∀ (i : ℤ), i ≠ 0 → g i ≤ f i
summablef : Summable f
f' : ℤ → ℝ := fun i => if i = 0 then g i else f i
f'def : f' = fun i => if i = 0 then g i else f i
this : ∀ (i : ℤ), g i ≤ f' i
s : Finset ℤ := {0}
b : ℤ
hb : b ∉ s
⊢ f' b = f b
Tactic:
rw [mem_singleton] at hb
Proof state after:
f g : ℤ → ℝ
hgpos : 0 ≤ g
hgf : ∀ (i : ℤ), i ≠ 0 → g i ≤ f i
summablef : Summable f
f' : ℤ → ℝ := fun i => if i = 0 then g i else f i
f'def : f' = fun i => if i = 0 then g i else f i
this : ∀ (i : ℤ), g i ≤ f' i
s : Finset ℤ := {0}
b : ℤ
hb : ¬b = 0
⊢ f' b = f b
Theorem: summable_of_le_on_nonzero
Proof state before:
f g : ℤ → ℝ
hgpos : 0 ≤ g
hgf : ∀ (i : ℤ), i ≠ 0 → g i ≤ f i
summablef : Summable f
f' : ℤ → ℝ := fun i => if i = 0 then g i else f i
f'def : f' = fun i => if i = 0 then g i else f i
this : ∀ (i : ℤ), g i ≤ f' i
s : Finset ℤ := {0}
b : ℤ
hb : ¬b = 0
⊢ f' b = f b
Tactic:
rw [f'def]
Proof state after:
f g : ℤ → ℝ
hgpos : 0 ≤ g
hgf : ∀ (i : ℤ), i ≠ 0 → g i ≤ f i
summablef : Summable f
f' : ℤ → ℝ := fun i => if i = 0 then g i else f i
f'def : f' = fun i => if i = 0 then g i else f i
this : ∀ (i : ℤ), g i ≤ f' i
s : Finset ℤ := {0}
b : ℤ
hb : ¬b = 0
⊢ (fun i => if i = 0 then g i else f i) b = f b
Theorem: summable_of_le_on_nonzero
Proof state before:
f g : ℤ → ℝ
hgpos : 0 ≤ g
hgf : ∀ (i : ℤ), i ≠ 0 → g i ≤ f i
summablef : Summable f
f' : ℤ → ℝ := fun i => if i = 0 then g i else f i
f'def : f' = fun i => if i = 0 then g i else f i
this : ∀ (i : ℤ), g i ≤ f' i
s : Finset ℤ := {0}
b : ℤ
hb : ¬b = 0
⊢ (fun i => if i = 0 then g i else f i) b = f b
Tactic:
simp [hb]
Proof state after:
no goals
Theorem: summable_of_le_on_nonzero
Proof state before:
f g : ℤ → ℝ
hgpos : 0 ≤ g
hgf : ∀ (i : ℤ), i ≠ 0 → g i ≤ f i
summablef : Summable f
f' : ℤ → ℝ := fun i => if i = 0 then g i else f i
f'def : f' = fun i => if i = 0 then g i else f i
⊢ ∀ (i : ℤ), g i ≤ f' i
Tactic:
intro i
Proof state after:
f g : ℤ → ℝ
hgpos : 0 ≤ g
hgf : ∀ (i : ℤ), i ≠ 0 → g i ≤ f i
summablef : Summable f
f' : ℤ → ℝ := fun i => if i = 0 then g i else f i
f'def : f' = fun i => if i = 0 then g i else f i
i : ℤ
⊢ g i ≤ f' i
Theorem: summable_of_le_on_nonzero
Proof state before:
f g : ℤ → ℝ
hgpos : 0 ≤ g
hgf : ∀ (i : ℤ), i ≠ 0 → g i ≤ f i
summablef : Summable f
f' : ℤ → ℝ := fun i => if i = 0 then g i else f i
f'def : f' = fun i => if i = 0 then g i else f i
i : ℤ
⊢ g i ≤ f' i
Tactic:
rw [f'def]
Proof state after:
f g : ℤ → ℝ
hgpos : 0 ≤ g
hgf : ∀ (i : ℤ), i ≠ 0 → g i ≤ f i
summablef : Summable f
f' : ℤ → ℝ := fun i => if i = 0 then g i else f i
f'def : f' = fun i => if i = 0 then g i else f i
i : ℤ
⊢ g i ≤ (fun i => if i = 0 then g i else f i) i
Theorem: summable_of_le_on_nonzero
Proof state before:
f g : ℤ → ℝ
hgpos : 0 ≤ g
hgf : ∀ (i : ℤ), i ≠ 0 → g i ≤ f i
summablef : Summable f
f' : ℤ → ℝ := fun i => if i = 0 then g i else f i
f'def : f' = fun i => if i = 0 then g i else f i
i : ℤ
⊢ g i ≤ (fun i => if i = 0 then g i else f i) i
Tactic:
by_cases h : i = 0
Proof state after:
case pos
f g : ℤ → ℝ
hgpos : 0 ≤ g
hgf : ∀ (i : ℤ), i ≠ 0 → g i ≤ f i
summablef : Summable f
f' : ℤ → ℝ := fun i => if i = 0 then g i else f i
f'def : f' = fun i => if i = 0 then g i else f i
i : ℤ
h : i = 0
⊢ g i ≤ (fun i => if i = 0 then g i else f i) i

case neg
f g : ℤ → ℝ
hgpos : 0 ≤ g
hgf : ∀ (i : ℤ), i ≠ 0 → g i ≤ f i
summablef : Summable f
f' : ℤ → ℝ := fun i => if i = 0 then g i else f i
f'def : f' = fun i => if i = 0 then g i else f i
i : ℤ
h : ¬i = 0
⊢ g i ≤ (fun i => if i = 0 then g i else f i) i
Theorem: summable_of_le_on_nonzero
Proof state before:
case pos
f g : ℤ → ℝ
hgpos : 0 ≤ g
hgf : ∀ (i : ℤ), i ≠ 0 → g i ≤ f i
summablef : Summable f
f' : ℤ → ℝ := fun i => if i = 0 then g i else f i
f'def : f' = fun i => if i = 0 then g i else f i
i : ℤ
h : i = 0
⊢ g i ≤ (fun i => if i = 0 then g i else f i) i

case neg
f g : ℤ → ℝ
hgpos : 0 ≤ g
hgf : ∀ (i : ℤ), i ≠ 0 → g i ≤ f i
summablef : Summable f
f' : ℤ → ℝ := fun i => if i = 0 then g i else f i
f'def : f' = fun i => if i = 0 then g i else f i
i : ℤ
h : ¬i = 0
⊢ g i ≤ (fun i => if i = 0 then g i else f i) i
Tactic:
. simp [h]
Proof state after:
case neg
f g : ℤ → ℝ
hgpos : 0 ≤ g
hgf : ∀ (i : ℤ), i ≠ 0 → g i ≤ f i
summablef : Summable f
f' : ℤ → ℝ := fun i => if i = 0 then g i else f i
f'def : f' = fun i => if i = 0 then g i else f i
i : ℤ
h : ¬i = 0
⊢ g i ≤ (fun i => if i = 0 then g i else f i) i
Theorem: summable_of_le_on_nonzero
Proof state before:
case neg
f g : ℤ → ℝ
hgpos : 0 ≤ g
hgf : ∀ (i : ℤ), i ≠ 0 → g i ≤ f i
summablef : Summable f
f' : ℤ → ℝ := fun i => if i = 0 then g i else f i
f'def : f' = fun i => if i = 0 then g i else f i
i : ℤ
h : ¬i = 0
⊢ g i ≤ (fun i => if i = 0 then g i else f i) i
Tactic:
. simp only [h, ↓reduceIte]
  exact hgf i h
Proof state after:
no goals
Theorem: summable_of_le_on_nonzero
Proof state before:
case pos
f g : ℤ → ℝ
hgpos : 0 ≤ g
hgf : ∀ (i : ℤ), i ≠ 0 → g i ≤ f i
summablef : Summable f
f' : ℤ → ℝ := fun i => if i = 0 then g i else f i
f'def : f' = fun i => if i = 0 then g i else f i
i : ℤ
h : i = 0
⊢ g i ≤ (fun i => if i = 0 then g i else f i) i
Tactic:
simp [h]
Proof state after:
no goals
Theorem: summable_of_le_on_nonzero
Proof state before:
case neg
f g : ℤ → ℝ
hgpos : 0 ≤ g
hgf : ∀ (i : ℤ), i ≠ 0 → g i ≤ f i
summablef : Summable f
f' : ℤ → ℝ := fun i => if i = 0 then g i else f i
f'def : f' = fun i => if i = 0 then g i else f i
i : ℤ
h : ¬i = 0
⊢ g i ≤ (fun i => if i = 0 then g i else f i) i
Tactic:
simp only [h, ↓reduceIte]
Proof state after:
case neg
f g : ℤ → ℝ
hgpos : 0 ≤ g
hgf : ∀ (i : ℤ), i ≠ 0 → g i ≤ f i
summablef : Summable f
f' : ℤ → ℝ := fun i => if i = 0 then g i else f i
f'def : f' = fun i => if i = 0 then g i else f i
i : ℤ
h : ¬i = 0
⊢ g i ≤ f i
Theorem: summable_of_le_on_nonzero
Proof state before:
case neg
f g : ℤ → ℝ
hgpos : 0 ≤ g
hgf : ∀ (i : ℤ), i ≠ 0 → g i ≤ f i
summablef : Summable f
f' : ℤ → ℝ := fun i => if i = 0 then g i else f i
f'def : f' = fun i => if i = 0 then g i else f i
i : ℤ
h : ¬i = 0
⊢ g i ≤ f i
Tactic:
exact hgf i h
Proof state after:
no goals
Theorem: continuous_bounded
Proof state before:
f : ℝ → ℂ
hf : ContinuousOn f (Set.Icc 0 (2 * Real.pi))
⊢ ∃ C, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
Tactic:
have interval_compact := (@isCompact_Icc ℝ _ _ _ 0 (2 * Real.pi))
Proof state after:
f : ℝ → ℂ
hf : ContinuousOn f (Set.Icc 0 (2 * Real.pi))
interval_compact : IsCompact (Set.Icc 0 (2 * Real.pi))
⊢ ∃ C, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
Theorem: continuous_bounded
Proof state before:
f : ℝ → ℂ
hf : ContinuousOn f (Set.Icc 0 (2 * Real.pi))
interval_compact : IsCompact (Set.Icc 0 (2 * Real.pi))
⊢ ∃ C, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
Tactic:
have abs_f_continuousOn := Complex.continuous_abs.comp_continuousOn hf
Proof state after:
f : ℝ → ℂ
hf : ContinuousOn f (Set.Icc 0 (2 * Real.pi))
interval_compact : IsCompact (Set.Icc 0 (2 * Real.pi))
abs_f_continuousOn : ContinuousOn (⇑Complex.abs ∘ f) (Set.Icc 0 (2 * Real.pi))
⊢ ∃ C, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
Theorem: continuous_bounded
Proof state before:
f : ℝ → ℂ
hf : ContinuousOn f (Set.Icc 0 (2 * Real.pi))
interval_compact : IsCompact (Set.Icc 0 (2 * Real.pi))
abs_f_continuousOn : ContinuousOn (⇑Complex.abs ∘ f) (Set.Icc 0 (2 * Real.pi))
⊢ ∃ C, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
Tactic:
obtain ⟨a, _, ha⟩ := interval_compact.exists_isMaxOn (Set.nonempty_Icc.mpr Real.two_pi_pos.le) abs_f_continuousOn
Proof state after:
case intro.intro
f : ℝ → ℂ
hf : ContinuousOn f (Set.Icc 0 (2 * Real.pi))
interval_compact : IsCompact (Set.Icc 0 (2 * Real.pi))
abs_f_continuousOn : ContinuousOn (⇑Complex.abs ∘ f) (Set.Icc 0 (2 * Real.pi))
a : ℝ
left✝ : a ∈ Set.Icc 0 (2 * Real.pi)
ha : IsMaxOn (⇑Complex.abs ∘ f) (Set.Icc 0 (2 * Real.pi)) a
⊢ ∃ C, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
Theorem: continuous_bounded
Proof state before:
case intro.intro
f : ℝ → ℂ
hf : ContinuousOn f (Set.Icc 0 (2 * Real.pi))
interval_compact : IsCompact (Set.Icc 0 (2 * Real.pi))
abs_f_continuousOn : ContinuousOn (⇑Complex.abs ∘ f) (Set.Icc 0 (2 * Real.pi))
a : ℝ
left✝ : a ∈ Set.Icc 0 (2 * Real.pi)
ha : IsMaxOn (⇑Complex.abs ∘ f) (Set.Icc 0 (2 * Real.pi)) a
⊢ ∃ C, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
Tactic:
set C := Complex.abs (f a) with C_def
Proof state after:
case intro.intro
f : ℝ → ℂ
hf : ContinuousOn f (Set.Icc 0 (2 * Real.pi))
interval_compact : IsCompact (Set.Icc 0 (2 * Real.pi))
abs_f_continuousOn : ContinuousOn (⇑Complex.abs ∘ f) (Set.Icc 0 (2 * Real.pi))
a : ℝ
left✝ : a ∈ Set.Icc 0 (2 * Real.pi)
ha : IsMaxOn (⇑Complex.abs ∘ f) (Set.Icc 0 (2 * Real.pi)) a
C : ℝ := Complex.abs (f a)
C_def : C = Complex.abs (f a)
⊢ ∃ C, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
Theorem: continuous_bounded
Proof state before:
case intro.intro
f : ℝ → ℂ
hf : ContinuousOn f (Set.Icc 0 (2 * Real.pi))
interval_compact : IsCompact (Set.Icc 0 (2 * Real.pi))
abs_f_continuousOn : ContinuousOn (⇑Complex.abs ∘ f) (Set.Icc 0 (2 * Real.pi))
a : ℝ
left✝ : a ∈ Set.Icc 0 (2 * Real.pi)
ha : IsMaxOn (⇑Complex.abs ∘ f) (Set.Icc 0 (2 * Real.pi)) a
C : ℝ := Complex.abs (f a)
C_def : C = Complex.abs (f a)
⊢ ∃ C, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
Tactic:
use C
Proof state after:
case h
f : ℝ → ℂ
hf : ContinuousOn f (Set.Icc 0 (2 * Real.pi))
interval_compact : IsCompact (Set.Icc 0 (2 * Real.pi))
abs_f_continuousOn : ContinuousOn (⇑Complex.abs ∘ f) (Set.Icc 0 (2 * Real.pi))
a : ℝ
left✝ : a ∈ Set.Icc 0 (2 * Real.pi)
ha : IsMaxOn (⇑Complex.abs ∘ f) (Set.Icc 0 (2 * Real.pi)) a
C : ℝ := Complex.abs (f a)
C_def : C = Complex.abs (f a)
⊢ ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
Theorem: continuous_bounded
Proof state before:
case h
f : ℝ → ℂ
hf : ContinuousOn f (Set.Icc 0 (2 * Real.pi))
interval_compact : IsCompact (Set.Icc 0 (2 * Real.pi))
abs_f_continuousOn : ContinuousOn (⇑Complex.abs ∘ f) (Set.Icc 0 (2 * Real.pi))
a : ℝ
left✝ : a ∈ Set.Icc 0 (2 * Real.pi)
ha : IsMaxOn (⇑Complex.abs ∘ f) (Set.Icc 0 (2 * Real.pi)) a
C : ℝ := Complex.abs (f a)
C_def : C = Complex.abs (f a)
⊢ ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
Tactic:
intro x hx
Proof state after:
case h
f : ℝ → ℂ
hf : ContinuousOn f (Set.Icc 0 (2 * Real.pi))
interval_compact : IsCompact (Set.Icc 0 (2 * Real.pi))
abs_f_continuousOn : ContinuousOn (⇑Complex.abs ∘ f) (Set.Icc 0 (2 * Real.pi))
a : ℝ
left✝ : a ∈ Set.Icc 0 (2 * Real.pi)
ha : IsMaxOn (⇑Complex.abs ∘ f) (Set.Icc 0 (2 * Real.pi)) a
C : ℝ := Complex.abs (f a)
C_def : C = Complex.abs (f a)
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
⊢ Complex.abs (f x) ≤ C
Theorem: continuous_bounded
Proof state before:
case h
f : ℝ → ℂ
hf : ContinuousOn f (Set.Icc 0 (2 * Real.pi))
interval_compact : IsCompact (Set.Icc 0 (2 * Real.pi))
abs_f_continuousOn : ContinuousOn (⇑Complex.abs ∘ f) (Set.Icc 0 (2 * Real.pi))
a : ℝ
left✝ : a ∈ Set.Icc 0 (2 * Real.pi)
ha : IsMaxOn (⇑Complex.abs ∘ f) (Set.Icc 0 (2 * Real.pi)) a
C : ℝ := Complex.abs (f a)
C_def : C = Complex.abs (f a)
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
⊢ Complex.abs (f x) ≤ C
Tactic:
rw [C_def]
Proof state after:
case h
f : ℝ → ℂ
hf : ContinuousOn f (Set.Icc 0 (2 * Real.pi))
interval_compact : IsCompact (Set.Icc 0 (2 * Real.pi))
abs_f_continuousOn : ContinuousOn (⇑Complex.abs ∘ f) (Set.Icc 0 (2 * Real.pi))
a : ℝ
left✝ : a ∈ Set.Icc 0 (2 * Real.pi)
ha : IsMaxOn (⇑Complex.abs ∘ f) (Set.Icc 0 (2 * Real.pi)) a
C : ℝ := Complex.abs (f a)
C_def : C = Complex.abs (f a)
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
⊢ Complex.abs (f x) ≤ Complex.abs (f a)
Theorem: continuous_bounded
Proof state before:
case h
f : ℝ → ℂ
hf : ContinuousOn f (Set.Icc 0 (2 * Real.pi))
interval_compact : IsCompact (Set.Icc 0 (2 * Real.pi))
abs_f_continuousOn : ContinuousOn (⇑Complex.abs ∘ f) (Set.Icc 0 (2 * Real.pi))
a : ℝ
left✝ : a ∈ Set.Icc 0 (2 * Real.pi)
ha : IsMaxOn (⇑Complex.abs ∘ f) (Set.Icc 0 (2 * Real.pi)) a
C : ℝ := Complex.abs (f a)
C_def : C = Complex.abs (f a)
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
⊢ Complex.abs (f x) ≤ Complex.abs (f a)
Tactic:
rw [isMaxOn_iff] at ha
Proof state after:
case h
f : ℝ → ℂ
hf : ContinuousOn f (Set.Icc 0 (2 * Real.pi))
interval_compact : IsCompact (Set.Icc 0 (2 * Real.pi))
abs_f_continuousOn : ContinuousOn (⇑Complex.abs ∘ f) (Set.Icc 0 (2 * Real.pi))
a : ℝ
left✝ : a ∈ Set.Icc 0 (2 * Real.pi)
ha : ∀ x ∈ Set.Icc 0 (2 * Real.pi), (⇑Complex.abs ∘ f) x ≤ (⇑Complex.abs ∘ f) a
C : ℝ := Complex.abs (f a)
C_def : C = Complex.abs (f a)
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
⊢ Complex.abs (f x) ≤ Complex.abs (f a)
Theorem: continuous_bounded
Proof state before:
case h
f : ℝ → ℂ
hf : ContinuousOn f (Set.Icc 0 (2 * Real.pi))
interval_compact : IsCompact (Set.Icc 0 (2 * Real.pi))
abs_f_continuousOn : ContinuousOn (⇑Complex.abs ∘ f) (Set.Icc 0 (2 * Real.pi))
a : ℝ
left✝ : a ∈ Set.Icc 0 (2 * Real.pi)
ha : ∀ x ∈ Set.Icc 0 (2 * Real.pi), (⇑Complex.abs ∘ f) x ≤ (⇑Complex.abs ∘ f) a
C : ℝ := Complex.abs (f a)
C_def : C = Complex.abs (f a)
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
⊢ Complex.abs (f x) ≤ Complex.abs (f a)
Tactic:
exact ha x hx
Proof state after:
no goals
Theorem: fourierCoeffOn_bound
Proof 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
Proof 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
Theorem: fourierCoeffOn_bound
Proof 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
Proof 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
Theorem: fourierCoeffOn_bound
Proof 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
Proof 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
Theorem: fourierCoeffOn_bound
Proof 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]
Proof 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
Theorem: fourierCoeffOn_bound
Proof 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]
Proof 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
Theorem: fourierCoeffOn_bound
Proof 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
Proof 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
Theorem: fourierCoeffOn_bound
Proof 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]
Proof 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)
Theorem: fourierCoeffOn_bound
Proof 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
Proof state after:
no goals
Theorem: fourierCoeffOn_bound
Proof 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
Proof 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
Theorem: fourierCoeffOn_bound
Proof 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
Proof 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
Theorem: fourierCoeffOn_bound
Proof 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
Proof 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
Theorem: fourierCoeffOn_bound
Proof 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
Proof 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
Theorem: fourierCoeffOn_bound
Proof 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]
Proof 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
Theorem: fourierCoeffOn_bound
Proof 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
Proof 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
Theorem: fourierCoeffOn_bound
Proof 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
Proof state after:
no goals