Theorem: integrableOn_mul_dirichletKernel'_max (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))
    (Set.Icc (x - Real.pi) (x + Real.pi)) MeasureTheory.volume
Tactic:
conv => pattern ((f _) * _ * _); rw [mul_assoc, mul_comm]
State after:
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 => ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y) * f y)
    (Set.Icc (x - Real.pi) (x + Real.pi)) MeasureTheory.volume

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 => ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y) * f y)
    (Set.Icc (x - Real.pi) (x + Real.pi)) MeasureTheory.volume
Tactic:
rw [intervalIntegrable_iff_integrableOn_Icc_of_le (by linarith [Real.pi_pos])] at hf
State after:
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : MeasureTheory.IntegrableOn f (Set.Icc (-Real.pi) (3 * Real.pi)) MeasureTheory.volume
N : ℕ
⊢ MeasureTheory.IntegrableOn (fun y => ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y) * f y)
    (Set.Icc (x - Real.pi) (x + Real.pi)) MeasureTheory.volume

State before:
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : MeasureTheory.IntegrableOn f (Set.Icc (-Real.pi) (3 * Real.pi)) MeasureTheory.volume
N : ℕ
⊢ MeasureTheory.IntegrableOn (fun y => ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y) * f y)
    (Set.Icc (x - Real.pi) (x + Real.pi)) MeasureTheory.volume
Tactic:
apply MeasureTheory.Integrable.bdd_mul'
State after:
case hg
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : MeasureTheory.IntegrableOn f (Set.Icc (-Real.pi) (3 * Real.pi)) MeasureTheory.volume
N : ℕ
⊢ MeasureTheory.Integrable (fun x => f x) (MeasureTheory.volume.restrict (Set.Icc (x - Real.pi) (x + Real.pi)))

case hf
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : MeasureTheory.IntegrableOn f (Set.Icc (-Real.pi) (3 * Real.pi)) MeasureTheory.volume
N : ℕ
⊢ MeasureTheory.AEStronglyMeasurable (fun x_1 => ↑(max (1 - |x - x_1|) 0) * dirichletKernel' N (x - x_1))
    (MeasureTheory.volume.restrict (Set.Icc (x - Real.pi) (x + Real.pi)))

case hf_bound
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : MeasureTheory.IntegrableOn f (Set.Icc (-Real.pi) (3 * Real.pi)) MeasureTheory.volume
N : ℕ
⊢ ∀ᵐ (x_1 : ℝ) ∂MeasureTheory.volume.restrict (Set.Icc (x - Real.pi) (x + Real.pi)),
    ‖↑(max (1 - |x - x_1|) 0) * dirichletKernel' N (x - x_1)‖ ≤ ?c

case c
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : MeasureTheory.IntegrableOn f (Set.Icc (-Real.pi) (3 * Real.pi)) MeasureTheory.volume
N : ℕ
⊢ ℝ

State before:
case hg
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : MeasureTheory.IntegrableOn f (Set.Icc (-Real.pi) (3 * Real.pi)) MeasureTheory.volume
N : ℕ
⊢ MeasureTheory.Integrable (fun x => f x) (MeasureTheory.volume.restrict (Set.Icc (x - Real.pi) (x + Real.pi)))

case hf
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : MeasureTheory.IntegrableOn f (Set.Icc (-Real.pi) (3 * Real.pi)) MeasureTheory.volume
N : ℕ
⊢ MeasureTheory.AEStronglyMeasurable (fun x_1 => ↑(max (1 - |x - x_1|) 0) * dirichletKernel' N (x - x_1))
    (MeasureTheory.volume.restrict (Set.Icc (x - Real.pi) (x + Real.pi)))

case hf_bound
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : MeasureTheory.IntegrableOn f (Set.Icc (-Real.pi) (3 * Real.pi)) MeasureTheory.volume
N : ℕ
⊢ ∀ᵐ (x_1 : ℝ) ∂MeasureTheory.volume.restrict (Set.Icc (x - Real.pi) (x + Real.pi)),
    ‖↑(max (1 - |x - x_1|) 0) * dirichletKernel' N (x - x_1)‖ ≤ ?c

case c
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : MeasureTheory.IntegrableOn f (Set.Icc (-Real.pi) (3 * Real.pi)) MeasureTheory.volume
N : ℕ
⊢ ℝ
Tactic:
. apply hf.mono_set
  intro y hy
  constructor <;> linarith [hx.1, hx.2, hy.1, hy.2, Real.two_le_pi]
State after:
case hf
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : MeasureTheory.IntegrableOn f (Set.Icc (-Real.pi) (3 * Real.pi)) MeasureTheory.volume
N : ℕ
⊢ MeasureTheory.AEStronglyMeasurable (fun x_1 => ↑(max (1 - |x - x_1|) 0) * dirichletKernel' N (x - x_1))
    (MeasureTheory.volume.restrict (Set.Icc (x - Real.pi) (x + Real.pi)))

case hf_bound
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : MeasureTheory.IntegrableOn f (Set.Icc (-Real.pi) (3 * Real.pi)) MeasureTheory.volume
N : ℕ
⊢ ∀ᵐ (x_1 : ℝ) ∂MeasureTheory.volume.restrict (Set.Icc (x - Real.pi) (x + Real.pi)),
    ‖↑(max (1 - |x - x_1|) 0) * dirichletKernel' N (x - x_1)‖ ≤ ?c

case c
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : MeasureTheory.IntegrableOn f (Set.Icc (-Real.pi) (3 * Real.pi)) MeasureTheory.volume
N : ℕ
⊢ ℝ

State before:
case hf
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : MeasureTheory.IntegrableOn f (Set.Icc (-Real.pi) (3 * Real.pi)) MeasureTheory.volume
N : ℕ
⊢ MeasureTheory.AEStronglyMeasurable (fun x_1 => ↑(max (1 - |x - x_1|) 0) * dirichletKernel' N (x - x_1))
    (MeasureTheory.volume.restrict (Set.Icc (x - Real.pi) (x + Real.pi)))

case hf_bound
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : MeasureTheory.IntegrableOn f (Set.Icc (-Real.pi) (3 * Real.pi)) MeasureTheory.volume
N : ℕ
⊢ ∀ᵐ (x_1 : ℝ) ∂MeasureTheory.volume.restrict (Set.Icc (x - Real.pi) (x + Real.pi)),
    ‖↑(max (1 - |x - x_1|) 0) * dirichletKernel' N (x - x_1)‖ ≤ ?c

case c
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : MeasureTheory.IntegrableOn f (Set.Icc (-Real.pi) (3 * Real.pi)) MeasureTheory.volume
N : ℕ
⊢ ℝ
Tactic:
. apply Measurable.aestronglyMeasurable
  apply Measurable.mul
  . apply Measurable.comp Complex.measurable_ofReal
    apply Measurable.max
    apply Measurable.const_sub
    apply Measurable.comp _root_.continuous_abs.measurable
    apply Measurable.const_sub measurable_id
    exact measurable_const
  . apply Measurable.comp dirichletKernel'_measurable
    apply Measurable.const_sub measurable_id
State after:
case hf_bound
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : MeasureTheory.IntegrableOn f (Set.Icc (-Real.pi) (3 * Real.pi)) MeasureTheory.volume
N : ℕ
⊢ ∀ᵐ (x_1 : ℝ) ∂MeasureTheory.volume.restrict (Set.Icc (x - Real.pi) (x + Real.pi)),
    ‖↑(max (1 - |x - x_1|) 0) * dirichletKernel' N (x - x_1)‖ ≤ ?c

case c
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : MeasureTheory.IntegrableOn f (Set.Icc (-Real.pi) (3 * Real.pi)) MeasureTheory.volume
N : ℕ
⊢ ℝ

State before:
case hf_bound
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : MeasureTheory.IntegrableOn f (Set.Icc (-Real.pi) (3 * Real.pi)) MeasureTheory.volume
N : ℕ
⊢ ∀ᵐ (x_1 : ℝ) ∂MeasureTheory.volume.restrict (Set.Icc (x - Real.pi) (x + Real.pi)),
    ‖↑(max (1 - |x - x_1|) 0) * dirichletKernel' N (x - x_1)‖ ≤ ?c

case c
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : MeasureTheory.IntegrableOn f (Set.Icc (-Real.pi) (3 * Real.pi)) MeasureTheory.volume
N : ℕ
⊢ ℝ
Tactic:
. rw [MeasureTheory.ae_restrict_iff' measurableSet_Icc]
  apply eventually_of_forall
  intro y _
  calc ‖(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)‖
    _ = ‖max (1 - |x - y|) 0‖ * ‖dirichletKernel' N (x - y)‖ := by
      rw [norm_mul, Complex.norm_real]
    _ ≤ 1 * (2 * N + 1) := by
      gcongr
      . rw [Real.norm_of_nonneg]
        apply max_le
        linarith [abs_nonneg (x - y)]
        norm_num
        apply le_max_right
      apply norm_dirichletKernel'_le
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 : ℕ
⊢ -Real.pi ≤ 3 * Real.pi
Tactic:
linarith [Real.pi_pos]
State after:
no goals

State before:
case hg
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : MeasureTheory.IntegrableOn f (Set.Icc (-Real.pi) (3 * Real.pi)) MeasureTheory.volume
N : ℕ
⊢ MeasureTheory.Integrable (fun x => f x) (MeasureTheory.volume.restrict (Set.Icc (x - Real.pi) (x + Real.pi)))
Tactic:
apply hf.mono_set
State after:
case hg
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : MeasureTheory.IntegrableOn f (Set.Icc (-Real.pi) (3 * Real.pi)) MeasureTheory.volume
N : ℕ
⊢ Set.Icc (x - Real.pi) (x + Real.pi) ⊆ Set.Icc (-Real.pi) (3 * Real.pi)

State before:
case hg
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : MeasureTheory.IntegrableOn f (Set.Icc (-Real.pi) (3 * Real.pi)) MeasureTheory.volume
N : ℕ
⊢ Set.Icc (x - Real.pi) (x + Real.pi) ⊆ Set.Icc (-Real.pi) (3 * Real.pi)
Tactic:
intro y hy
State after:
case hg
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : MeasureTheory.IntegrableOn f (Set.Icc (-Real.pi) (3 * Real.pi)) MeasureTheory.volume
N : ℕ
y : ℝ
hy : y ∈ Set.Icc (x - Real.pi) (x + Real.pi)
⊢ y ∈ Set.Icc (-Real.pi) (3 * Real.pi)

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

State before:
case hf
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : MeasureTheory.IntegrableOn f (Set.Icc (-Real.pi) (3 * Real.pi)) MeasureTheory.volume
N : ℕ
⊢ MeasureTheory.AEStronglyMeasurable (fun x_1 => ↑(max (1 - |x - x_1|) 0) * dirichletKernel' N (x - x_1))
    (MeasureTheory.volume.restrict (Set.Icc (x - Real.pi) (x + Real.pi)))
Tactic:
apply Measurable.aestronglyMeasurable
State after:
case hf.hf
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : MeasureTheory.IntegrableOn f (Set.Icc (-Real.pi) (3 * Real.pi)) MeasureTheory.volume
N : ℕ
⊢ Measurable fun x_1 => ↑(max (1 - |x - x_1|) 0) * dirichletKernel' N (x - x_1)

State before:
case hf.hf
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : MeasureTheory.IntegrableOn f (Set.Icc (-Real.pi) (3 * Real.pi)) MeasureTheory.volume
N : ℕ
⊢ Measurable fun x_1 => ↑(max (1 - |x - x_1|) 0) * dirichletKernel' N (x - x_1)
Tactic:
apply Measurable.mul
State after:
case hf.hf.hf
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : MeasureTheory.IntegrableOn f (Set.Icc (-Real.pi) (3 * Real.pi)) MeasureTheory.volume
N : ℕ
⊢ Measurable fun a => ↑(max (1 - |x - a|) 0)

case hf.hf.hg
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : MeasureTheory.IntegrableOn f (Set.Icc (-Real.pi) (3 * Real.pi)) MeasureTheory.volume
N : ℕ
⊢ Measurable fun a => dirichletKernel' N (x - a)

State before:
case hf.hf.hf
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : MeasureTheory.IntegrableOn f (Set.Icc (-Real.pi) (3 * Real.pi)) MeasureTheory.volume
N : ℕ
⊢ Measurable fun a => ↑(max (1 - |x - a|) 0)

case hf.hf.hg
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : MeasureTheory.IntegrableOn f (Set.Icc (-Real.pi) (3 * Real.pi)) MeasureTheory.volume
N : ℕ
⊢ Measurable fun a => dirichletKernel' N (x - a)
Tactic:
. apply Measurable.comp Complex.measurable_ofReal
  apply Measurable.max
  apply Measurable.const_sub
  apply Measurable.comp _root_.continuous_abs.measurable
  apply Measurable.const_sub measurable_id
  exact measurable_const
State after:
case hf.hf.hg
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : MeasureTheory.IntegrableOn f (Set.Icc (-Real.pi) (3 * Real.pi)) MeasureTheory.volume
N : ℕ
⊢ Measurable fun a => dirichletKernel' N (x - a)

State before:
case hf.hf.hg
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : MeasureTheory.IntegrableOn f (Set.Icc (-Real.pi) (3 * Real.pi)) MeasureTheory.volume
N : ℕ
⊢ Measurable fun a => dirichletKernel' N (x - a)
Tactic:
. apply Measurable.comp dirichletKernel'_measurable
  apply Measurable.const_sub measurable_id
State after:
no goals

State before:
case hf.hf.hf
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : MeasureTheory.IntegrableOn f (Set.Icc (-Real.pi) (3 * Real.pi)) MeasureTheory.volume
N : ℕ
⊢ Measurable fun a => ↑(max (1 - |x - a|) 0)
Tactic:
apply Measurable.comp Complex.measurable_ofReal
State after:
case hf.hf.hf
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : MeasureTheory.IntegrableOn f (Set.Icc (-Real.pi) (3 * Real.pi)) MeasureTheory.volume
N : ℕ
⊢ Measurable fun a => max (1 - |x - a|) 0

State before:
case hf.hf.hf
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : MeasureTheory.IntegrableOn f (Set.Icc (-Real.pi) (3 * Real.pi)) MeasureTheory.volume
N : ℕ
⊢ Measurable fun a => max (1 - |x - a|) 0
Tactic:
apply Measurable.max
State after:
case hf.hf.hf.hf
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : MeasureTheory.IntegrableOn f (Set.Icc (-Real.pi) (3 * Real.pi)) MeasureTheory.volume
N : ℕ
⊢ Measurable fun a => 1 - |x - a|

case hf.hf.hf.hg
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : MeasureTheory.IntegrableOn f (Set.Icc (-Real.pi) (3 * Real.pi)) MeasureTheory.volume
N : ℕ
⊢ Measurable fun a => 0

State before:
case hf.hf.hf.hf
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : MeasureTheory.IntegrableOn f (Set.Icc (-Real.pi) (3 * Real.pi)) MeasureTheory.volume
N : ℕ
⊢ Measurable fun a => 1 - |x - a|

case hf.hf.hf.hg
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : MeasureTheory.IntegrableOn f (Set.Icc (-Real.pi) (3 * Real.pi)) MeasureTheory.volume
N : ℕ
⊢ Measurable fun a => 0
Tactic:
apply Measurable.const_sub
State after:
case hf.hf.hf.hf.hf
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : MeasureTheory.IntegrableOn f (Set.Icc (-Real.pi) (3 * Real.pi)) MeasureTheory.volume
N : ℕ
⊢ Measurable fun x_1 => |x - x_1|

case hf.hf.hf.hg
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : MeasureTheory.IntegrableOn f (Set.Icc (-Real.pi) (3 * Real.pi)) MeasureTheory.volume
N : ℕ
⊢ Measurable fun a => 0

State before:
case hf.hf.hf.hf.hf
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : MeasureTheory.IntegrableOn f (Set.Icc (-Real.pi) (3 * Real.pi)) MeasureTheory.volume
N : ℕ
⊢ Measurable fun x_1 => |x - x_1|

case hf.hf.hf.hg
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : MeasureTheory.IntegrableOn f (Set.Icc (-Real.pi) (3 * Real.pi)) MeasureTheory.volume
N : ℕ
⊢ Measurable fun a => 0
Tactic:
apply Measurable.comp _root_.continuous_abs.measurable
State after:
case hf.hf.hf.hf.hf
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : MeasureTheory.IntegrableOn f (Set.Icc (-Real.pi) (3 * Real.pi)) MeasureTheory.volume
N : ℕ
⊢ Measurable fun x_1 => x - x_1

case hf.hf.hf.hg
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : MeasureTheory.IntegrableOn f (Set.Icc (-Real.pi) (3 * Real.pi)) MeasureTheory.volume
N : ℕ
⊢ Measurable fun a => 0

State before:
case hf.hf.hf.hf.hf
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : MeasureTheory.IntegrableOn f (Set.Icc (-Real.pi) (3 * Real.pi)) MeasureTheory.volume
N : ℕ
⊢ Measurable fun x_1 => x - x_1

case hf.hf.hf.hg
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : MeasureTheory.IntegrableOn f (Set.Icc (-Real.pi) (3 * Real.pi)) MeasureTheory.volume
N : ℕ
⊢ Measurable fun a => 0
Tactic:
apply Measurable.const_sub measurable_id
State after:
case hf.hf.hf.hg
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : MeasureTheory.IntegrableOn f (Set.Icc (-Real.pi) (3 * Real.pi)) MeasureTheory.volume
N : ℕ
⊢ Measurable fun a => 0

State before:
case hf.hf.hf.hg
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : MeasureTheory.IntegrableOn f (Set.Icc (-Real.pi) (3 * Real.pi)) MeasureTheory.volume
N : ℕ
⊢ Measurable fun a => 0
Tactic:
exact measurable_const
State after:
no goals

State before:
case hf.hf.hg
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : MeasureTheory.IntegrableOn f (Set.Icc (-Real.pi) (3 * Real.pi)) MeasureTheory.volume
N : ℕ
⊢ Measurable fun a => dirichletKernel' N (x - a)
Tactic:
apply Measurable.comp dirichletKernel'_measurable
State after:
case hf.hf.hg
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : MeasureTheory.IntegrableOn f (Set.Icc (-Real.pi) (3 * Real.pi)) MeasureTheory.volume
N : ℕ
⊢ Measurable fun a => x - a

State before:
case hf.hf.hg
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : MeasureTheory.IntegrableOn f (Set.Icc (-Real.pi) (3 * Real.pi)) MeasureTheory.volume
N : ℕ
⊢ Measurable fun a => x - a
Tactic:
apply Measurable.const_sub measurable_id
State after:
no goals

State before:
case hf_bound
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : MeasureTheory.IntegrableOn f (Set.Icc (-Real.pi) (3 * Real.pi)) MeasureTheory.volume
N : ℕ
⊢ ∀ᵐ (x_1 : ℝ) ∂MeasureTheory.volume.restrict (Set.Icc (x - Real.pi) (x + Real.pi)),
    ‖↑(max (1 - |x - x_1|) 0) * dirichletKernel' N (x - x_1)‖ ≤ ?c
Tactic:
rw [MeasureTheory.ae_restrict_iff' measurableSet_Icc]
State after:
case hf_bound
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : MeasureTheory.IntegrableOn f (Set.Icc (-Real.pi) (3 * Real.pi)) MeasureTheory.volume
N : ℕ
⊢ ∀ᵐ (x_1 : ℝ),
    x_1 ∈ Set.Icc (x - Real.pi) (x + Real.pi) → ‖↑(max (1 - |x - x_1|) 0) * dirichletKernel' N (x - x_1)‖ ≤ ?c

case c
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : MeasureTheory.IntegrableOn f (Set.Icc (-Real.pi) (3 * Real.pi)) MeasureTheory.volume
N : ℕ
⊢ ℝ

State before:
case hf_bound
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : MeasureTheory.IntegrableOn f (Set.Icc (-Real.pi) (3 * Real.pi)) MeasureTheory.volume
N : ℕ
⊢ ∀ᵐ (x_1 : ℝ),
    x_1 ∈ Set.Icc (x - Real.pi) (x + Real.pi) → ‖↑(max (1 - |x - x_1|) 0) * dirichletKernel' N (x - x_1)‖ ≤ ?c

case c
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : MeasureTheory.IntegrableOn f (Set.Icc (-Real.pi) (3 * Real.pi)) MeasureTheory.volume
N : ℕ
⊢ ℝ
Tactic:
apply eventually_of_forall
State after:
case hf_bound.hp
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : MeasureTheory.IntegrableOn f (Set.Icc (-Real.pi) (3 * Real.pi)) MeasureTheory.volume
N : ℕ
⊢ ∀ x_1 ∈ Set.Icc (x - Real.pi) (x + Real.pi), ‖↑(max (1 - |x - x_1|) 0) * dirichletKernel' N (x - x_1)‖ ≤ ?c

case c
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : MeasureTheory.IntegrableOn f (Set.Icc (-Real.pi) (3 * Real.pi)) MeasureTheory.volume
N : ℕ
⊢ ℝ

State before:
case hf_bound.hp
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : MeasureTheory.IntegrableOn f (Set.Icc (-Real.pi) (3 * Real.pi)) MeasureTheory.volume
N : ℕ
⊢ ∀ x_1 ∈ Set.Icc (x - Real.pi) (x + Real.pi), ‖↑(max (1 - |x - x_1|) 0) * dirichletKernel' N (x - x_1)‖ ≤ ?c

case c
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : MeasureTheory.IntegrableOn f (Set.Icc (-Real.pi) (3 * Real.pi)) MeasureTheory.volume
N : ℕ
⊢ ℝ
Tactic:
intro y _
State after:
case hf_bound.hp
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : MeasureTheory.IntegrableOn f (Set.Icc (-Real.pi) (3 * Real.pi)) MeasureTheory.volume
N : ℕ
y : ℝ
a✝ : y ∈ Set.Icc (x - Real.pi) (x + Real.pi)
⊢ ‖↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)‖ ≤ ?c

case c
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : MeasureTheory.IntegrableOn f (Set.Icc (-Real.pi) (3 * Real.pi)) MeasureTheory.volume
N : ℕ
⊢ ℝ

State before:
case hf_bound.hp
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : MeasureTheory.IntegrableOn f (Set.Icc (-Real.pi) (3 * Real.pi)) MeasureTheory.volume
N : ℕ
y : ℝ
a✝ : y ∈ Set.Icc (x - Real.pi) (x + Real.pi)
⊢ ‖↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)‖ ≤ ?c

case c
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : MeasureTheory.IntegrableOn f (Set.Icc (-Real.pi) (3 * Real.pi)) MeasureTheory.volume
N : ℕ
⊢ ℝ
Tactic:
calc ‖(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)‖
  _ = ‖max (1 - |x - y|) 0‖ * ‖dirichletKernel' N (x - y)‖ := by
    rw [norm_mul, Complex.norm_real]
  _ ≤ 1 * (2 * N + 1) := by
    gcongr
    . rw [Real.norm_of_nonneg]
      apply max_le
      linarith [abs_nonneg (x - y)]
      norm_num
      apply le_max_right
    apply norm_dirichletKernel'_le
State after:
no goals

State before:
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : MeasureTheory.IntegrableOn f (Set.Icc (-Real.pi) (3 * Real.pi)) MeasureTheory.volume
N : ℕ
y : ℝ
a✝ : y ∈ Set.Icc (x - Real.pi) (x + Real.pi)
⊢ ‖↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)‖ = ‖max (1 - |x - y|) 0‖ * ‖dirichletKernel' N (x - y)‖
Tactic:
rw [norm_mul, Complex.norm_real]
State after:
no goals

State before:
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : MeasureTheory.IntegrableOn f (Set.Icc (-Real.pi) (3 * Real.pi)) MeasureTheory.volume
N : ℕ
y : ℝ
a✝ : y ∈ Set.Icc (x - Real.pi) (x + Real.pi)
⊢ ‖max (1 - |x - y|) 0‖ * ‖dirichletKernel' N (x - y)‖ ≤ 1 * (2 * ↑N + 1)
Tactic:
gcongr
State after:
case h₁
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : MeasureTheory.IntegrableOn f (Set.Icc (-Real.pi) (3 * Real.pi)) MeasureTheory.volume
N : ℕ
y : ℝ
a✝ : y ∈ Set.Icc (x - Real.pi) (x + Real.pi)
⊢ ‖max (1 - |x - y|) 0‖ ≤ 1

case h₂
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : MeasureTheory.IntegrableOn f (Set.Icc (-Real.pi) (3 * Real.pi)) MeasureTheory.volume
N : ℕ
y : ℝ
a✝ : y ∈ Set.Icc (x - Real.pi) (x + Real.pi)
⊢ ‖dirichletKernel' N (x - y)‖ ≤ 2 * ↑N + 1

State before:
case h₁
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : MeasureTheory.IntegrableOn f (Set.Icc (-Real.pi) (3 * Real.pi)) MeasureTheory.volume
N : ℕ
y : ℝ
a✝ : y ∈ Set.Icc (x - Real.pi) (x + Real.pi)
⊢ ‖max (1 - |x - y|) 0‖ ≤ 1

case h₂
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : MeasureTheory.IntegrableOn f (Set.Icc (-Real.pi) (3 * Real.pi)) MeasureTheory.volume
N : ℕ
y : ℝ
a✝ : y ∈ Set.Icc (x - Real.pi) (x + Real.pi)
⊢ ‖dirichletKernel' N (x - y)‖ ≤ 2 * ↑N + 1
Tactic:
. rw [Real.norm_of_nonneg]
  apply max_le
  linarith [abs_nonneg (x - y)]
  norm_num
  apply le_max_right
State after:
case h₂
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : MeasureTheory.IntegrableOn f (Set.Icc (-Real.pi) (3 * Real.pi)) MeasureTheory.volume
N : ℕ
y : ℝ
a✝ : y ∈ Set.Icc (x - Real.pi) (x + Real.pi)
⊢ ‖dirichletKernel' N (x - y)‖ ≤ 2 * ↑N + 1

State before:
case h₂
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : MeasureTheory.IntegrableOn f (Set.Icc (-Real.pi) (3 * Real.pi)) MeasureTheory.volume
N : ℕ
y : ℝ
a✝ : y ∈ Set.Icc (x - Real.pi) (x + Real.pi)
⊢ ‖dirichletKernel' N (x - y)‖ ≤ 2 * ↑N + 1
Tactic:
apply norm_dirichletKernel'_le
State after:
no goals

State before:
case h₁
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : MeasureTheory.IntegrableOn f (Set.Icc (-Real.pi) (3 * Real.pi)) MeasureTheory.volume
N : ℕ
y : ℝ
a✝ : y ∈ Set.Icc (x - Real.pi) (x + Real.pi)
⊢ ‖max (1 - |x - y|) 0‖ ≤ 1
Tactic:
rw [Real.norm_of_nonneg]
State after:
case h₁
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : MeasureTheory.IntegrableOn f (Set.Icc (-Real.pi) (3 * Real.pi)) MeasureTheory.volume
N : ℕ
y : ℝ
a✝ : y ∈ Set.Icc (x - Real.pi) (x + Real.pi)
⊢ max (1 - |x - y|) 0 ≤ 1

case h₁
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : MeasureTheory.IntegrableOn f (Set.Icc (-Real.pi) (3 * Real.pi)) MeasureTheory.volume
N : ℕ
y : ℝ
a✝ : y ∈ Set.Icc (x - Real.pi) (x + Real.pi)
⊢ 0 ≤ max (1 - |x - y|) 0

State before:
case h₁
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : MeasureTheory.IntegrableOn f (Set.Icc (-Real.pi) (3 * Real.pi)) MeasureTheory.volume
N : ℕ
y : ℝ
a✝ : y ∈ Set.Icc (x - Real.pi) (x + Real.pi)
⊢ max (1 - |x - y|) 0 ≤ 1

case h₁
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : MeasureTheory.IntegrableOn f (Set.Icc (-Real.pi) (3 * Real.pi)) MeasureTheory.volume
N : ℕ
y : ℝ
a✝ : y ∈ Set.Icc (x - Real.pi) (x + Real.pi)
⊢ 0 ≤ max (1 - |x - y|) 0
Tactic:
apply max_le
State after:
case h₁.h₁
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : MeasureTheory.IntegrableOn f (Set.Icc (-Real.pi) (3 * Real.pi)) MeasureTheory.volume
N : ℕ
y : ℝ
a✝ : y ∈ Set.Icc (x - Real.pi) (x + Real.pi)
⊢ 1 - |x - y| ≤ 1

case h₁.h₂
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : MeasureTheory.IntegrableOn f (Set.Icc (-Real.pi) (3 * Real.pi)) MeasureTheory.volume
N : ℕ
y : ℝ
a✝ : y ∈ Set.Icc (x - Real.pi) (x + Real.pi)
⊢ 0 ≤ 1

case h₁
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : MeasureTheory.IntegrableOn f (Set.Icc (-Real.pi) (3 * Real.pi)) MeasureTheory.volume
N : ℕ
y : ℝ
a✝ : y ∈ Set.Icc (x - Real.pi) (x + Real.pi)
⊢ 0 ≤ max (1 - |x - y|) 0

State before:
case h₁.h₁
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : MeasureTheory.IntegrableOn f (Set.Icc (-Real.pi) (3 * Real.pi)) MeasureTheory.volume
N : ℕ
y : ℝ
a✝ : y ∈ Set.Icc (x - Real.pi) (x + Real.pi)
⊢ 1 - |x - y| ≤ 1

case h₁.h₂
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : MeasureTheory.IntegrableOn f (Set.Icc (-Real.pi) (3 * Real.pi)) MeasureTheory.volume
N : ℕ
y : ℝ
a✝ : y ∈ Set.Icc (x - Real.pi) (x + Real.pi)
⊢ 0 ≤ 1

case h₁
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : MeasureTheory.IntegrableOn f (Set.Icc (-Real.pi) (3 * Real.pi)) MeasureTheory.volume
N : ℕ
y : ℝ
a✝ : y ∈ Set.Icc (x - Real.pi) (x + Real.pi)
⊢ 0 ≤ max (1 - |x - y|) 0
Tactic:
linarith [abs_nonneg (x - y)]
State after:
case h₁.h₂
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : MeasureTheory.IntegrableOn f (Set.Icc (-Real.pi) (3 * Real.pi)) MeasureTheory.volume
N : ℕ
y : ℝ
a✝ : y ∈ Set.Icc (x - Real.pi) (x + Real.pi)
⊢ 0 ≤ 1

case h₁
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : MeasureTheory.IntegrableOn f (Set.Icc (-Real.pi) (3 * Real.pi)) MeasureTheory.volume
N : ℕ
y : ℝ
a✝ : y ∈ Set.Icc (x - Real.pi) (x + Real.pi)
⊢ 0 ≤ max (1 - |x - y|) 0

State before:
case h₁.h₂
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : MeasureTheory.IntegrableOn f (Set.Icc (-Real.pi) (3 * Real.pi)) MeasureTheory.volume
N : ℕ
y : ℝ
a✝ : y ∈ Set.Icc (x - Real.pi) (x + Real.pi)
⊢ 0 ≤ 1

case h₁
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : MeasureTheory.IntegrableOn f (Set.Icc (-Real.pi) (3 * Real.pi)) MeasureTheory.volume
N : ℕ
y : ℝ
a✝ : y ∈ Set.Icc (x - Real.pi) (x + Real.pi)
⊢ 0 ≤ max (1 - |x - y|) 0
Tactic:
norm_num
State after:
case h₁
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : MeasureTheory.IntegrableOn f (Set.Icc (-Real.pi) (3 * Real.pi)) MeasureTheory.volume
N : ℕ
y : ℝ
a✝ : y ∈ Set.Icc (x - Real.pi) (x + Real.pi)
⊢ 0 ≤ max (1 - |x - y|) 0

State before:
case h₁
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : MeasureTheory.IntegrableOn f (Set.Icc (-Real.pi) (3 * Real.pi)) MeasureTheory.volume
N : ℕ
y : ℝ
a✝ : y ∈ Set.Icc (x - Real.pi) (x + Real.pi)
⊢ 0 ≤ max (1 - |x - y|) 0
Tactic:
apply le_max_right
State after:
no goals