internlm/Lean-Github huggingface dataset:
Theorem: integrableOn_mul_dirichletKernel'_min
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 : ℕ
⊢ 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 : ℕ
⊢ ℝ
Tactic:
. apply hf.mono_set
  intro y hy
  constructor <;> linarith [hx.1, hx.2, hy.1, hy.2, Real.two_le_pi]
Proof 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 => ↑(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 : ℕ
⊢ ℝ
Theorem: integrableOn_mul_dirichletKernel'_min
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 => ↑(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 : ℕ
⊢ ℝ
Tactic:
. apply Measurable.aestronglyMeasurable
  apply Measurable.mul
  . apply Measurable.comp Complex.measurable_ofReal
    apply Measurable.min
    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
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 : ℝ) ∂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 : ℕ
⊢ ℝ
Theorem: integrableOn_mul_dirichletKernel'_min
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)),
    ‖↑(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 : ℕ
⊢ ℝ
Tactic:
. rw [MeasureTheory.ae_restrict_iff' measurableSet_Icc]
  apply eventually_of_forall
  intro y _
  calc ‖(min |x - y| 1) * dirichletKernel' N (x - y)‖
    _ = ‖min |x - y| 1‖ * ‖dirichletKernel' N (x - y)‖ := by
      rw [norm_mul, Complex.norm_real]
    _ ≤ 1 * (2 * N + 1) := by
      gcongr
      . rw [Real.norm_of_nonneg]
        apply min_le_right
        apply le_min
        linarith [abs_nonneg (x - y)]
        norm_num
      apply norm_dirichletKernel'_le
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 : ℕ
⊢ -Real.pi ≤ 3 * Real.pi
Tactic:
linarith [Real.pi_pos]
Proof state after:
no goals
Theorem: integrableOn_mul_dirichletKernel'_min
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 : ℕ
⊢ MeasureTheory.Integrable (fun x => f x) (MeasureTheory.volume.restrict (Set.Icc (x - Real.pi) (x + Real.pi)))
Tactic:
apply hf.mono_set
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 : ℕ
⊢ Set.Icc (x - Real.pi) (x + Real.pi) ⊆ Set.Icc (-Real.pi) (3 * Real.pi)
Theorem: integrableOn_mul_dirichletKernel'_min
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'_min
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'_min
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 => ↑(min |x - x_1| 1) * 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 => ↑(min |x - x_1| 1) * dirichletKernel' N (x - x_1)
Theorem: integrableOn_mul_dirichletKernel'_min
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 => ↑(min |x - x_1| 1) * 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 => ↑(min |x - a| 1)

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'_min
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 => ↑(min |x - a| 1)

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.min
  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'_min
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'_min
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 => ↑(min |x - a| 1)
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 => min |x - a| 1
Theorem: integrableOn_mul_dirichletKernel'_min
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 => min |x - a| 1
Tactic:
apply Measurable.min
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 => |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 => 1
Theorem: integrableOn_mul_dirichletKernel'_min
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 => |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 => 1
Tactic:
apply Measurable.comp _root_.continuous_abs.measurable
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 => 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 => 1
Theorem: integrableOn_mul_dirichletKernel'_min
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 => 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 => 1
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 => 1
Theorem: integrableOn_mul_dirichletKernel'_min
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 => 1
Tactic:
exact measurable_const
Proof state after:
no goals
Theorem: integrableOn_mul_dirichletKernel'_min
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'_min
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'_min
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)),
    ‖↑(min |x - x_1| 1) * 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) → ‖↑(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 : ℕ
⊢ ℝ
Theorem: integrableOn_mul_dirichletKernel'_min
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) → ‖↑(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 : ℕ
⊢ ℝ
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), ‖↑(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 : ℕ
⊢ ℝ
Theorem: integrableOn_mul_dirichletKernel'_min
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), ‖↑(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 : ℕ
⊢ ℝ
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)
⊢ ‖↑(min |x - y| 1) * 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'_min
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)
⊢ ‖↑(min |x - y| 1) * 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 ‖(min |x - y| 1) * dirichletKernel' N (x - y)‖
  _ = ‖min |x - y| 1‖ * ‖dirichletKernel' N (x - y)‖ := by
    rw [norm_mul, Complex.norm_real]
  _ ≤ 1 * (2 * N + 1) := by
    gcongr
    . rw [Real.norm_of_nonneg]
      apply min_le_right
      apply le_min
      linarith [abs_nonneg (x - y)]
      norm_num
    apply norm_dirichletKernel'_le
Proof state after:
no goals
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 : ℕ
y : ℝ
a✝ : y ∈ Set.Icc (x - Real.pi) (x + Real.pi)
⊢ ‖↑(min |x - y| 1) * dirichletKernel' N (x - y)‖ = ‖min |x - y| 1‖ * ‖dirichletKernel' N (x - y)‖
Tactic:
rw [norm_mul, Complex.norm_real]
Proof state after:
no goals
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 : ℕ
y : ℝ
a✝ : y ∈ Set.Icc (x - Real.pi) (x + Real.pi)
⊢ ‖min |x - y| 1‖ * ‖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)
⊢ ‖min |x - y| 1‖ ≤ 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'_min
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)
⊢ ‖min |x - y| 1‖ ≤ 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 min_le_right
  apply le_min
  linarith [abs_nonneg (x - y)]
  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)
⊢ ‖dirichletKernel' N (x - y)‖ ≤ 2 * ↑N + 1
Theorem: integrableOn_mul_dirichletKernel'_min
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'_min
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)
⊢ ‖min |x - y| 1‖ ≤ 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)
⊢ min |x - y| 1 ≤ 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 ≤ min |x - y| 1
Theorem: integrableOn_mul_dirichletKernel'_min
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)
⊢ min |x - y| 1 ≤ 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 ≤ min |x - y| 1
Tactic:
apply min_le_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)
⊢ 0 ≤ min |x - y| 1
Theorem: integrableOn_mul_dirichletKernel'_min
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 ≤ min |x - y| 1
Tactic:
apply le_min
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 ≤ |x - y|

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
Theorem: integrableOn_mul_dirichletKernel'_min
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 ≤ |x - y|

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
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
Theorem: integrableOn_mul_dirichletKernel'_min
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
Tactic:
norm_num
Proof state after:
no goals
Theorem: integrableOn_mul_dirichletKernel'_specific
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 * ↑(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
Proof 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)
Theorem: integrableOn_mul_dirichletKernel'_specific
Proof 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
Proof 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)