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

State before:
f g : ℤ → ℝ
hgpos : 0 ≤ g
hgf : ∀ (i : ℤ), i ≠ 0 → g i ≤ f i
summablef : Summable f
⊢ Summable g
Tactic:
set f' : ℤ → ℝ := fun i ↦ if i = 0 then g i else f i with f'def
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
⊢ Summable g

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
⊢ Summable g
Tactic:
have : ∀ i, g i ≤ f' i := by
  intro i
  rw [f'def]
  by_cases h : i = 0
  . simp [h]
  . simp only [h, ↓reduceIte]
    exact hgf i h
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
⊢ Summable g

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
⊢ Summable g
Tactic:
apply Real.summable_of_le hgpos this
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
⊢ Summable fun b => f' b

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
⊢ Summable fun b => f' b
Tactic:
let s : Finset ℤ := {0}
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}
⊢ Summable fun b => f' b

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}
⊢ Summable fun b => f' b
Tactic:
rw [←s.summable_compl_iff]
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}
⊢ Summable fun x => f' ↑x

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}
⊢ Summable fun x => f' ↑x
Tactic:
apply (summable_congr _).mpr (s.summable_compl_iff.mpr summablef)
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 : { x // x ∉ s }), f' ↑b = f ↑b

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

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

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

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

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

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

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

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

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

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

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

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

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