Theorem: integrableOn_mul_dirichletKernel'_specific (Carleson/Theorem1_1/Control_Approximation_Effect.lean)

State before:
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
⊢ MeasureTheory.IntegrableOn (fun y => f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y))
    {y | dist x y ∈ Set.Ioo 0 1} MeasureTheory.volume
Tactic:
apply (integrableOn_mul_dirichletKernel'_max hx hf).mono_set
State after:
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
⊢ {y | dist x y ∈ Set.Ioo 0 1} ⊆ Set.Icc (x - Real.pi) (x + Real.pi)

State before:
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
⊢ {y | dist x y ∈ Set.Ioo 0 1} ⊆ Set.Icc (x - Real.pi) (x + Real.pi)
Tactic:
intro y hy
State after:
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
y : ℝ
hy : y ∈ {y | dist x y ∈ Set.Ioo 0 1}
⊢ y ∈ Set.Icc (x - Real.pi) (x + Real.pi)

State before:
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
y : ℝ
hy : y ∈ {y | dist x y ∈ Set.Ioo 0 1}
⊢ y ∈ Set.Icc (x - Real.pi) (x + Real.pi)
Tactic:
rw [annulus_real_eq (by rfl)] at hy
State after:
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
y : ℝ
hy : y ∈ Set.Ioo (x - 1) (x - 0) ∪ Set.Ioo (x + 0) (x + 1)
⊢ y ∈ Set.Icc (x - Real.pi) (x + Real.pi)

State before:
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
y : ℝ
hy : y ∈ Set.Ioo (x - 1) (x - 0) ∪ Set.Ioo (x + 0) (x + 1)
⊢ y ∈ Set.Icc (x - Real.pi) (x + Real.pi)
Tactic:
rcases hy with h | h <;> constructor <;> linarith [h.1, h.2, hx.1, hx.2, Real.two_le_pi]
State after:
no goals

State before:
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
y : ℝ
hy : y ∈ {y | dist x y ∈ Set.Ioo 0 1}
⊢ 0 ≤ 0
Tactic:
rfl
State after:
no goals