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

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))
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

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
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

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
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

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
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

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
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

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
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

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]
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)

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
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)

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
State after:
no goals