internlm/Lean-Github huggingface dataset:
Theorem: integrableOn_mul_dirichletKernel'_max
Proof 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
Proof 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)
Theorem: integrableOn_mul_dirichletKernel'_max
Proof 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]
Proof state after:
no goals
Theorem: integrableOn_mul_dirichletKernel'_max
Proof 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
Proof 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)
Theorem: integrableOn_mul_dirichletKernel'_max
Proof 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
Proof 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)
Theorem: integrableOn_mul_dirichletKernel'_max
Proof 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
Proof 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)
Theorem: integrableOn_mul_dirichletKernel'_max
Proof 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
Proof state after:
no goals
Theorem: integrableOn_mul_dirichletKernel'_max
Proof 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
Proof 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
Theorem: integrableOn_mul_dirichletKernel'_max
Proof 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
Proof 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
Theorem: integrableOn_mul_dirichletKernel'_max
Proof 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
Proof 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
Theorem: integrableOn_mul_dirichletKernel'_max
Proof 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
Proof 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
Theorem: integrableOn_mul_dirichletKernel'_max
Proof 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
Proof 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
Theorem: integrableOn_mul_dirichletKernel'_max
Proof 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
Proof state after:
no goals
Theorem: integrableOn_mul_dirichletKernel'_max
Proof 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
Proof 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
Theorem: integrableOn_mul_dirichletKernel'_max
Proof 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
Proof state after:
no goals
Theorem: integrableOn_mul_dirichletKernel'_max
Proof 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]
Proof 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 : ℕ
⊢ ℝ
Theorem: integrableOn_mul_dirichletKernel'_max
Proof 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
Proof 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 : ℕ
⊢ ℝ
Theorem: integrableOn_mul_dirichletKernel'_max
Proof 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 _
Proof 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 : ℕ
⊢ ℝ
Theorem: integrableOn_mul_dirichletKernel'_max
Proof 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
Proof state after:
no goals
Theorem: integrableOn_mul_dirichletKernel'_max
Proof 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]
Proof state after:
no goals
Theorem: integrableOn_mul_dirichletKernel'_max
Proof 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
Proof 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
Theorem: integrableOn_mul_dirichletKernel'_max
Proof 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
Proof 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
Theorem: integrableOn_mul_dirichletKernel'_max
Proof 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
Proof state after:
no goals
Theorem: integrableOn_mul_dirichletKernel'_max
Proof 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]
Proof 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
Theorem: integrableOn_mul_dirichletKernel'_max
Proof 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
Proof 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
Theorem: integrableOn_mul_dirichletKernel'_max
Proof 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)]
Proof 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
Theorem: integrableOn_mul_dirichletKernel'_max
Proof 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
Proof 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
Theorem: integrableOn_mul_dirichletKernel'_max
Proof 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
Proof state after:
no goals
Theorem: integrableOn_mul_dirichletKernel'_min
Proof 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 * ↑(min |x - y| 1) * dirichletKernel' N (x - y))
    (Set.Icc (x - Real.pi) (x + Real.pi)) MeasureTheory.volume
Tactic:
conv => pattern ((f _) * _ * _); rw [mul_assoc, mul_comm]
Proof 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 => ↑(min |x - y| 1) * dirichletKernel' N (x - y) * f y)
    (Set.Icc (x - Real.pi) (x + Real.pi)) MeasureTheory.volume
Theorem: integrableOn_mul_dirichletKernel'_min
Proof 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 => ↑(min |x - y| 1) * 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
Proof 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 => ↑(min |x - y| 1) * dirichletKernel' N (x - y) * f y)
    (Set.Icc (x - Real.pi) (x + Real.pi)) MeasureTheory.volume
Theorem: integrableOn_mul_dirichletKernel'_min
Proof 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 => ↑(min |x - y| 1) * dirichletKernel' N (x - y) * f y)
    (Set.Icc (x - Real.pi) (x + Real.pi)) MeasureTheory.volume
Tactic:
apply MeasureTheory.Integrable.bdd_mul'
Proof 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 => ↑(min |x - x_1| 1) * 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)),
    ‖↑(min |x - x_1| 1) * 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 : ℕ
⊢ ℝ