internlm/Lean-Github huggingface dataset:
Theorem: intervalIntegral.integral_conj'
Proof state before:
μ : MeasureTheory.Measure ℝ
𝕜 : Type
inst✝ : RCLike 𝕜
f : ℝ → 𝕜
a b : ℝ
⊢ ↑(if a ≤ b then 1 else -1) * (starRingEnd 𝕜) (∫ (x : ℝ) in Ι a b, f x ∂μ) =
    (starRingEnd 𝕜) ↑(if a ≤ b then 1 else -1) * (starRingEnd 𝕜) (∫ (x : ℝ) in Ι a b, f x ∂μ)
Tactic:
congr
Proof state after:
case e_a
μ : MeasureTheory.Measure ℝ
𝕜 : Type
inst✝ : RCLike 𝕜
f : ℝ → 𝕜
a b : ℝ
⊢ ↑(if a ≤ b then 1 else -1) = (starRingEnd 𝕜) ↑(if a ≤ b then 1 else -1)
Theorem: intervalIntegral.integral_conj'
Proof state before:
case e_a
μ : MeasureTheory.Measure ℝ
𝕜 : Type
inst✝ : RCLike 𝕜
f : ℝ → 𝕜
a b : ℝ
⊢ ↑(if a ≤ b then 1 else -1) = (starRingEnd 𝕜) ↑(if a ≤ b then 1 else -1)
Tactic:
simp
Proof state after:
no goals
Theorem: dirichlet_Hilbert_eq
Proof state before:
N : ℕ
x y : ℝ
⊢ ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y) =
    cexp (I * (-↑N * ↑x)) * K x y * cexp (I * ↑N * ↑y) +
      (starRingEnd ℂ) (cexp (I * (-↑N * ↑x)) * K x y * cexp (I * ↑N * ↑y))
Tactic:
rw [dirichletKernel', K, k]
Proof state after:
N : ℕ
x y : ℝ
⊢ ↑(max (1 - |x - y|) 0) *
      (cexp (I * ↑N * ↑(x - y)) / (1 - cexp (-I * ↑(x - y))) + cexp (-I * ↑N * ↑(x - y)) / (1 - cexp (I * ↑(x - y)))) =
    cexp (I * (-↑N * ↑x)) * (↑(max (1 - |x - y|) 0) / (1 - cexp (I * ↑(x - y)))) * cexp (I * ↑N * ↑y) +
      (starRingEnd ℂ)
        (cexp (I * (-↑N * ↑x)) * (↑(max (1 - |x - y|) 0) / (1 - cexp (I * ↑(x - y)))) * cexp (I * ↑N * ↑y))
Theorem: dirichlet_Hilbert_eq
Proof state before:
N : ℕ
x y : ℝ
⊢ ↑(max (1 - |x - y|) 0) *
      (cexp (I * ↑N * ↑(x - y)) / (1 - cexp (-I * ↑(x - y))) + cexp (-I * ↑N * ↑(x - y)) / (1 - cexp (I * ↑(x - y)))) =
    cexp (I * (-↑N * ↑x)) * (↑(max (1 - |x - y|) 0) / (1 - cexp (I * ↑(x - y)))) * cexp (I * ↑N * ↑y) +
      (starRingEnd ℂ)
        (cexp (I * (-↑N * ↑x)) * (↑(max (1 - |x - y|) 0) / (1 - cexp (I * ↑(x - y)))) * cexp (I * ↑N * ↑y))
Tactic:
rw [map_mul, map_mul, map_div₀, conj_ofReal, map_sub, ←exp_conj, ←exp_conj, ←exp_conj,
  map_mul, map_mul, map_mul, map_mul, map_mul, conj_ofReal, conj_ofReal, conj_ofReal]
Proof state after:
N : ℕ
x y : ℝ
⊢ ↑(max (1 - |x - y|) 0) *
      (cexp (I * ↑N * ↑(x - y)) / (1 - cexp (-I * ↑(x - y))) + cexp (-I * ↑N * ↑(x - y)) / (1 - cexp (I * ↑(x - y)))) =
    cexp (I * (-↑N * ↑x)) * (↑(max (1 - |x - y|) 0) / (1 - cexp (I * ↑(x - y)))) * cexp (I * ↑N * ↑y) +
      cexp ((starRingEnd ℂ) I * ((starRingEnd ℂ) (-↑N) * ↑x)) *
          (↑(max (1 - |x - y|) 0) / ((starRingEnd ℂ) 1 - cexp ((starRingEnd ℂ) I * ↑(x - y)))) *
        cexp ((starRingEnd ℂ) I * (starRingEnd ℂ) ↑N * ↑y)
Theorem: dirichlet_Hilbert_eq
Proof state before:
N : ℕ
x y : ℝ
⊢ ↑(max (1 - |x - y|) 0) *
      (cexp (I * ↑N * ↑(x - y)) / (1 - cexp (-I * ↑(x - y))) + cexp (-I * ↑N * ↑(x - y)) / (1 - cexp (I * ↑(x - y)))) =
    cexp (I * (-↑N * ↑x)) * (↑(max (1 - |x - y|) 0) / (1 - cexp (I * ↑(x - y)))) * cexp (I * ↑N * ↑y) +
      cexp ((starRingEnd ℂ) I * ((starRingEnd ℂ) (-↑N) * ↑x)) *
          (↑(max (1 - |x - y|) 0) / ((starRingEnd ℂ) 1 - cexp ((starRingEnd ℂ) I * ↑(x - y)))) *
        cexp ((starRingEnd ℂ) I * (starRingEnd ℂ) ↑N * ↑y)
Tactic:
simp
Proof state after:
N : ℕ
x y : ℝ
⊢ ↑(max (1 - |x - y|) 0) *
      (cexp (I * ↑N * (↑x - ↑y)) / (1 - cexp (-(I * (↑x - ↑y)))) +
        cexp (-(I * ↑N * (↑x - ↑y))) / (1 - cexp (I * (↑x - ↑y)))) =
    cexp (-(I * (↑N * ↑x))) * (↑(max (1 - |x - y|) 0) / (1 - cexp (I * (↑x - ↑y)))) * cexp (I * ↑N * ↑y) +
      cexp (I * (↑N * ↑x)) * (↑(max (1 - |x - y|) 0) / (1 - cexp (-(I * (↑x - ↑y))))) * cexp (-(I * ↑N * ↑y))
Theorem: dirichlet_Hilbert_eq
Proof state before:
N : ℕ
x y : ℝ
⊢ ↑(max (1 - |x - y|) 0) *
      (cexp (I * ↑N * (↑x - ↑y)) / (1 - cexp (-(I * (↑x - ↑y)))) +
        cexp (-(I * ↑N * (↑x - ↑y))) / (1 - cexp (I * (↑x - ↑y)))) =
    cexp (-(I * (↑N * ↑x))) * (↑(max (1 - |x - y|) 0) / (1 - cexp (I * (↑x - ↑y)))) * cexp (I * ↑N * ↑y) +
      cexp (I * (↑N * ↑x)) * (↑(max (1 - |x - y|) 0) / (1 - cexp (-(I * (↑x - ↑y))))) * cexp (-(I * ↑N * ↑y))
Tactic:
field_simp
Proof state after:
N : ℕ
x y : ℝ
⊢ ↑(max (1 - |x - y|) 0) *
      (cexp (I * ↑N * (↑x - ↑y)) / (1 - cexp (-(I * (↑x - ↑y)))) +
        cexp (-(I * ↑N * (↑x - ↑y))) / (1 - cexp (I * (↑x - ↑y)))) =
    cexp (-(I * (↑N * ↑x))) * ↑(max (1 - |x - y|) 0) * cexp (I * ↑N * ↑y) / (1 - cexp (I * (↑x - ↑y))) +
      cexp (I * (↑N * ↑x)) * ↑(max (1 - |x - y|) 0) * cexp (-(I * ↑N * ↑y)) / (1 - cexp (-(I * (↑x - ↑y))))
Theorem: dirichlet_Hilbert_eq
Proof state before:
N : ℕ
x y : ℝ
⊢ ↑(max (1 - |x - y|) 0) *
      (cexp (I * ↑N * (↑x - ↑y)) / (1 - cexp (-(I * (↑x - ↑y)))) +
        cexp (-(I * ↑N * (↑x - ↑y))) / (1 - cexp (I * (↑x - ↑y)))) =
    cexp (-(I * (↑N * ↑x))) * ↑(max (1 - |x - y|) 0) * cexp (I * ↑N * ↑y) / (1 - cexp (I * (↑x - ↑y))) +
      cexp (I * (↑N * ↑x)) * ↑(max (1 - |x - y|) 0) * cexp (-(I * ↑N * ↑y)) / (1 - cexp (-(I * (↑x - ↑y))))
Tactic:
symm
Proof state after:
N : ℕ
x y : ℝ
⊢ cexp (-(I * (↑N * ↑x))) * ↑(max (1 - |x - y|) 0) * cexp (I * ↑N * ↑y) / (1 - cexp (I * (↑x - ↑y))) +
      cexp (I * (↑N * ↑x)) * ↑(max (1 - |x - y|) 0) * cexp (-(I * ↑N * ↑y)) / (1 - cexp (-(I * (↑x - ↑y)))) =
    ↑(max (1 - |x - y|) 0) *
      (cexp (I * ↑N * (↑x - ↑y)) / (1 - cexp (-(I * (↑x - ↑y)))) +
        cexp (-(I * ↑N * (↑x - ↑y))) / (1 - cexp (I * (↑x - ↑y))))
Theorem: dirichlet_Hilbert_eq
Proof state before:
N : ℕ
x y : ℝ
⊢ cexp (-(I * (↑N * ↑x))) * ↑(max (1 - |x - y|) 0) * cexp (I * ↑N * ↑y) / (1 - cexp (I * (↑x - ↑y))) +
      cexp (I * (↑N * ↑x)) * ↑(max (1 - |x - y|) 0) * cexp (-(I * ↑N * ↑y)) / (1 - cexp (-(I * (↑x - ↑y)))) =
    ↑(max (1 - |x - y|) 0) *
      (cexp (I * ↑N * (↑x - ↑y)) / (1 - cexp (-(I * (↑x - ↑y)))) +
        cexp (-(I * ↑N * (↑x - ↑y))) / (1 - cexp (I * (↑x - ↑y))))
Tactic:
rw [mul_comm, ←mul_assoc, ←exp_add, mul_comm, add_comm, mul_comm, ←mul_assoc, ←exp_add, mul_comm, mul_add, mul_div_assoc, mul_div_assoc]
Proof state after:
N : ℕ
x y : ℝ
⊢ ↑(max (1 - |x - y|) 0) * (cexp (-(I * ↑N * ↑y) + I * (↑N * ↑x)) / (1 - cexp (-(I * (↑x - ↑y))))) +
      ↑(max (1 - |x - y|) 0) * (cexp (I * ↑N * ↑y + -(I * (↑N * ↑x))) / (1 - cexp (I * (↑x - ↑y)))) =
    ↑(max (1 - |x - y|) 0) * (cexp (I * ↑N * (↑x - ↑y)) / (1 - cexp (-(I * (↑x - ↑y))))) +
      ↑(max (1 - |x - y|) 0) * (cexp (-(I * ↑N * (↑x - ↑y))) / (1 - cexp (I * (↑x - ↑y))))
Theorem: dirichlet_Hilbert_eq
Proof state before:
N : ℕ
x y : ℝ
⊢ ↑(max (1 - |x - y|) 0) * (cexp (-(I * ↑N * ↑y) + I * (↑N * ↑x)) / (1 - cexp (-(I * (↑x - ↑y))))) +
      ↑(max (1 - |x - y|) 0) * (cexp (I * ↑N * ↑y + -(I * (↑N * ↑x))) / (1 - cexp (I * (↑x - ↑y)))) =
    ↑(max (1 - |x - y|) 0) * (cexp (I * ↑N * (↑x - ↑y)) / (1 - cexp (-(I * (↑x - ↑y))))) +
      ↑(max (1 - |x - y|) 0) * (cexp (-(I * ↑N * (↑x - ↑y))) / (1 - cexp (I * (↑x - ↑y))))
Tactic:
congr <;> ring
Proof state after:
no goals
Theorem: le_iSup_of_tendsto
Proof state before:
α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : CompleteLinearOrder α
inst✝² : OrderTopology α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → α
a : α
ha : Tendsto f atTop (𝓝 a)
⊢ a ≤ iSup f
Tactic:
apply le_of_forall_lt
Proof state after:
case H
α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : CompleteLinearOrder α
inst✝² : OrderTopology α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → α
a : α
ha : Tendsto f atTop (𝓝 a)
⊢ ∀ c < a, c < iSup f
Theorem: le_iSup_of_tendsto
Proof state before:
case H
α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : CompleteLinearOrder α
inst✝² : OrderTopology α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → α
a : α
ha : Tendsto f atTop (𝓝 a)
⊢ ∀ c < a, c < iSup f
Tactic:
intro c hc
Proof state after:
case H
α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : CompleteLinearOrder α
inst✝² : OrderTopology α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → α
a : α
ha : Tendsto f atTop (𝓝 a)
c : α
hc : c < a
⊢ c < iSup f
Theorem: le_iSup_of_tendsto
Proof state before:
case H
α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : CompleteLinearOrder α
inst✝² : OrderTopology α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → α
a : α
ha : Tendsto f atTop (𝓝 a)
c : α
hc : c < a
⊢ c < iSup f
Tactic:
have : ∀ᶠ (x : β) in atTop, c < f x := by
  apply eventually_gt_of_tendsto_gt hc ha
Proof state after:
case H
α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : CompleteLinearOrder α
inst✝² : OrderTopology α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → α
a : α
ha : Tendsto f atTop (𝓝 a)
c : α
hc : c < a
this : ∀ᶠ (x : β) in atTop, c < f x
⊢ c < iSup f
Theorem: le_iSup_of_tendsto
Proof state before:
case H
α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : CompleteLinearOrder α
inst✝² : OrderTopology α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → α
a : α
ha : Tendsto f atTop (𝓝 a)
c : α
hc : c < a
this : ∀ᶠ (x : β) in atTop, c < f x
⊢ c < iSup f
Tactic:
rcases this.exists with ⟨x, hx⟩
Proof state after:
case H.intro
α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : CompleteLinearOrder α
inst✝² : OrderTopology α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → α
a : α
ha : Tendsto f atTop (𝓝 a)
c : α
hc : c < a
this : ∀ᶠ (x : β) in atTop, c < f x
x : β
hx : c < f x
⊢ c < iSup f
Theorem: le_iSup_of_tendsto
Proof state before:
case H.intro
α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : CompleteLinearOrder α
inst✝² : OrderTopology α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → α
a : α
ha : Tendsto f atTop (𝓝 a)
c : α
hc : c < a
this : ∀ᶠ (x : β) in atTop, c < f x
x : β
hx : c < f x
⊢ c < iSup f
Tactic:
apply lt_of_lt_of_le hx
Proof state after:
case H.intro
α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : CompleteLinearOrder α
inst✝² : OrderTopology α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → α
a : α
ha : Tendsto f atTop (𝓝 a)
c : α
hc : c < a
this : ∀ᶠ (x : β) in atTop, c < f x
x : β
hx : c < f x
⊢ f x ≤ iSup f
Theorem: le_iSup_of_tendsto
Proof state before:
case H.intro
α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : CompleteLinearOrder α
inst✝² : OrderTopology α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → α
a : α
ha : Tendsto f atTop (𝓝 a)
c : α
hc : c < a
this : ∀ᶠ (x : β) in atTop, c < f x
x : β
hx : c < f x
⊢ f x ≤ iSup f
Tactic:
apply le_iSup
Proof state after:
no goals
Theorem: le_iSup_of_tendsto
Proof state before:
α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : CompleteLinearOrder α
inst✝² : OrderTopology α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → α
a : α
ha : Tendsto f atTop (𝓝 a)
c : α
hc : c < a
⊢ ∀ᶠ (x : β) in atTop, c < f x
Tactic:
apply eventually_gt_of_tendsto_gt hc ha
Proof state after:
no goals
Theorem: integrable_annulus
Proof state before:
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
r : ℝ
r_nonneg : 0 ≤ r
rle1 : r < 1
⊢ MeasureTheory.Integrable (fun x => f x) (MeasureTheory.volume.restrict {y | dist x y ∈ Set.Ioo r 1})
Tactic:
rw [← MeasureTheory.IntegrableOn, annulus_real_eq r_nonneg]
Proof state after:
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
r : ℝ
r_nonneg : 0 ≤ r
rle1 : r < 1
⊢ MeasureTheory.IntegrableOn (fun x => f x) (Set.Ioo (x - 1) (x - r) ∪ Set.Ioo (x + r) (x + 1)) MeasureTheory.volume
Theorem: integrable_annulus
Proof state before:
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
r : ℝ
r_nonneg : 0 ≤ r
rle1 : r < 1
⊢ MeasureTheory.IntegrableOn (fun x => f x) (Set.Ioo (x - 1) (x - r) ∪ Set.Ioo (x + r) (x + 1)) MeasureTheory.volume
Tactic:
apply MeasureTheory.IntegrableOn.union <;>
. rw [← intervalIntegrable_iff_integrableOn_Ioo_of_le (by linarith)]
  apply hf.mono_set
  rw [Set.uIcc_of_le (by linarith), Set.uIcc_of_le (by linarith [Real.pi_pos])]
  intro y hy
  constructor <;> linarith [hx.1, hx.2, hy.1, hy.2, Real.two_le_pi]
Proof state after:
no goals
Theorem: integrable_annulus
Proof state before:
case ht
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
r : ℝ
r_nonneg : 0 ≤ r
rle1 : r < 1
⊢ MeasureTheory.IntegrableOn (fun x => f x) (Set.Ioo (x + r) (x + 1)) MeasureTheory.volume
Tactic:
rw [← intervalIntegrable_iff_integrableOn_Ioo_of_le (by linarith)]
Proof state after:
case ht
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
r : ℝ
r_nonneg : 0 ≤ r
rle1 : r < 1
⊢ IntervalIntegrable (fun x => f x) MeasureTheory.volume (x + r) (x + 1)
Theorem: integrable_annulus
Proof state before:
case ht
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
r : ℝ
r_nonneg : 0 ≤ r
rle1 : r < 1
⊢ IntervalIntegrable (fun x => f x) MeasureTheory.volume (x + r) (x + 1)
Tactic:
apply hf.mono_set
Proof state after:
case ht
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
r : ℝ
r_nonneg : 0 ≤ r
rle1 : r < 1
⊢ Set.uIcc (x + r) (x + 1) ⊆ Set.uIcc (-Real.pi) (3 * Real.pi)
Theorem: integrable_annulus
Proof state before:
case ht
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
r : ℝ
r_nonneg : 0 ≤ r
rle1 : r < 1
⊢ Set.uIcc (x + r) (x + 1) ⊆ Set.uIcc (-Real.pi) (3 * Real.pi)
Tactic:
rw [Set.uIcc_of_le (by linarith), Set.uIcc_of_le (by linarith [Real.pi_pos])]
Proof state after:
case ht
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
r : ℝ
r_nonneg : 0 ≤ r
rle1 : r < 1
⊢ Set.Icc (x + r) (x + 1) ⊆ Set.Icc (-Real.pi) (3 * Real.pi)
Theorem: integrable_annulus
Proof state before:
case ht
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
r : ℝ
r_nonneg : 0 ≤ r
rle1 : r < 1
⊢ Set.Icc (x + r) (x + 1) ⊆ Set.Icc (-Real.pi) (3 * Real.pi)
Tactic:
intro y hy
Proof state after:
case ht
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
r : ℝ
r_nonneg : 0 ≤ r
rle1 : r < 1
y : ℝ
hy : y ∈ Set.Icc (x + r) (x + 1)
⊢ y ∈ Set.Icc (-Real.pi) (3 * Real.pi)
Theorem: integrable_annulus
Proof state before:
case ht
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
r : ℝ
r_nonneg : 0 ≤ r
rle1 : r < 1
y : ℝ
hy : y ∈ Set.Icc (x + r) (x + 1)
⊢ 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: integrable_annulus
Proof state before:
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
r : ℝ
r_nonneg : 0 ≤ r
rle1 : r < 1
⊢ x + r ≤ x + 1
Tactic:
linarith
Proof state after:
no goals
Theorem: integrable_annulus
Proof state before:
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
r : ℝ
r_nonneg : 0 ≤ r
rle1 : r < 1
⊢ -Real.pi ≤ 3 * Real.pi
Tactic:
linarith [Real.pi_pos]
Proof state after:
no goals
Theorem: integrableOn_mul_dirichletKernel'_max
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))
    (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 => ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y) * f y)
    (Set.Icc (x - Real.pi) (x + Real.pi)) MeasureTheory.volume
Theorem: integrableOn_mul_dirichletKernel'_max
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 => ↑(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
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 => ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y) * f y)
    (Set.Icc (x - Real.pi) (x + Real.pi)) MeasureTheory.volume
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 : ℕ
⊢ 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'
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 => ↑(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 : ℕ
⊢ ℝ
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 : ℕ
⊢ 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]
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 => ↑(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 : ℕ
⊢ ℝ
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)))

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
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)),
    ‖↑(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 : ℝ) ∂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
Proof state after:
no goals
Theorem: integrableOn_mul_dirichletKernel'_max
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'_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 : ℕ
⊢ 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)