internlm/Lean-Github huggingface dataset:
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 : ℝ
hy : y ∈ {y | dist x y ∈ Set.Ioo 0 1}
⊢ y ∈ Set.Icc (x - Real.pi) (x + Real.pi)
Tactic:
rw [annulus_real_eq (by rfl)] at hy
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 ∈ Set.Ioo (x - 1) (x - 0) ∪ Set.Ioo (x + 0) (x + 1)
⊢ y ∈ 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 : ℝ
hy : y ∈ Set.Ioo (x - 1) (x - 0) ∪ Set.Ioo (x + 0) (x + 1)
⊢ y ∈ Set.Icc (x - Real.pi) (x + Real.pi)
Tactic:
rcases hy with h | h <;> constructor <;> linarith [h.1, h.2, hx.1, hx.2, Real.two_le_pi]
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 : ℕ
y : ℝ
hy : y ∈ {y | dist x y ∈ Set.Ioo 0 1}
⊢ 0 ≤ 0
Tactic:
rfl
Proof state after:
no goals
Theorem: le_CarlesonOperatorReal'
Proof state before:
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
⊢ ∀ x ∈ Set.Icc 0 (2 * Real.pi),
    ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo 0 1}, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)‖₊ ≤
      T' f x + T' (⇑(starRingEnd ℂ) ∘ f) x
Tactic:
intro x hx
Proof state after:
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
⊢ ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo 0 1}, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)‖₊ ≤
    T' f x + T' (⇑(starRingEnd ℂ) ∘ f) x
Theorem: le_CarlesonOperatorReal'
Proof state before:
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
⊢ ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo 0 1}, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)‖₊ ≤
    T' f x + T' (⇑(starRingEnd ℂ) ∘ f) x
Tactic:
set s : ℕ → Set ℝ := fun n ↦ {y | dist x y ∈ Set.Ioo (1 / (n + 2 : ℝ)) 1} with sdef
Proof state after:
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
s : ℕ → Set ℝ := fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
sdef : s = fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
⊢ ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo 0 1}, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)‖₊ ≤
    T' f x + T' (⇑(starRingEnd ℂ) ∘ f) x
Theorem: le_CarlesonOperatorReal'
Proof state before:
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
s : ℕ → Set ℝ := fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
sdef : s = fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
⊢ ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo 0 1}, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)‖₊ ≤
    T' f x + T' (⇑(starRingEnd ℂ) ∘ f) x
Tactic:
have hs : {y | dist x y ∈ Set.Ioo 0 1} = ⋃ n, s n := by
  ext y
  constructor
  . intro hy
    rw [Set.mem_setOf_eq, Set.mem_Ioo] at hy
    obtain ⟨n, hn⟩ := exists_nat_gt (1 / dist x y)
    simp
    use n
    rw [sdef]
    simp
    constructor
    . rw [inv_lt, inv_eq_one_div]
      apply lt_trans hn
      linarith
      linarith
      exact hy.1
    . exact hy.2
  . intro hy
    simp at hy
    rcases hy with ⟨n, hn⟩
    rw [sdef] at hn
    simp at hn
    constructor
    . apply lt_trans' hn.1
      norm_num
      linarith
    . exact hn.2
Proof state after:
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
s : ℕ → Set ℝ := fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
sdef : s = fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
hs : {y | dist x y ∈ Set.Ioo 0 1} = ⋃ n, s n
⊢ ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo 0 1}, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)‖₊ ≤
    T' f x + T' (⇑(starRingEnd ℂ) ∘ f) x
Theorem: le_CarlesonOperatorReal'
Proof state before:
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
s : ℕ → Set ℝ := fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
sdef : s = fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
hs : {y | dist x y ∈ Set.Ioo 0 1} = ⋃ n, s n
⊢ ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo 0 1}, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)‖₊ ≤
    T' f x + T' (⇑(starRingEnd ℂ) ∘ f) x
Tactic:
have : Tendsto (fun i => ∫ y in s i, f y * (max (1 - |x - y|) 0) * dirichletKernel' N (x - y)) atTop (𝓝 (∫ y in ⋃ n, s n, f y * (max (1 - |x - y|) 0) * dirichletKernel' N (x - y))) := by
  apply MeasureTheory.tendsto_setIntegral_of_monotone
  . intro n
    exact annulus_measurableSet
  . intro n m nlem
    simp
    intro y hy
    rw [sdef]
    rw [sdef] at hy
    simp
    simp at hy
    constructor
    . apply lt_of_le_of_lt _ hy.1
      rw [inv_le_inv]
      norm_cast
      all_goals linarith
    . exact hy.2
  . rw [← hs]
    exact integrableOn_mul_dirichletKernel'_specific hx hf
Proof state after:
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
s : ℕ → Set ℝ := fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
sdef : s = fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
hs : {y | dist x y ∈ Set.Ioo 0 1} = ⋃ n, s n
this :
  Tendsto (fun i => ∫ (y : ℝ) in s i, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)) atTop
    (𝓝 (∫ (y : ℝ) in ⋃ n, s n, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)))
⊢ ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo 0 1}, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)‖₊ ≤
    T' f x + T' (⇑(starRingEnd ℂ) ∘ f) x
Theorem: le_CarlesonOperatorReal'
Proof state before:
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
s : ℕ → Set ℝ := fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
sdef : s = fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
⊢ {y | dist x y ∈ Set.Ioo 0 1} = ⋃ n, s n
Tactic:
ext y
Proof state after:
case h
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
s : ℕ → Set ℝ := fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
sdef : s = fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
y : ℝ
⊢ y ∈ {y | dist x y ∈ Set.Ioo 0 1} ↔ y ∈ ⋃ n, s n
Theorem: le_CarlesonOperatorReal'
Proof state before:
case h
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
s : ℕ → Set ℝ := fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
sdef : s = fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
y : ℝ
⊢ y ∈ {y | dist x y ∈ Set.Ioo 0 1} ↔ y ∈ ⋃ n, s n
Tactic:
constructor
Proof state after:
case h.mp
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
s : ℕ → Set ℝ := fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
sdef : s = fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
y : ℝ
⊢ y ∈ {y | dist x y ∈ Set.Ioo 0 1} → y ∈ ⋃ n, s n

case h.mpr
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
s : ℕ → Set ℝ := fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
sdef : s = fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
y : ℝ
⊢ y ∈ ⋃ n, s n → y ∈ {y | dist x y ∈ Set.Ioo 0 1}
Theorem: le_CarlesonOperatorReal'
Proof state before:
case h.mp
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
s : ℕ → Set ℝ := fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
sdef : s = fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
y : ℝ
⊢ y ∈ {y | dist x y ∈ Set.Ioo 0 1} → y ∈ ⋃ n, s n

case h.mpr
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
s : ℕ → Set ℝ := fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
sdef : s = fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
y : ℝ
⊢ y ∈ ⋃ n, s n → y ∈ {y | dist x y ∈ Set.Ioo 0 1}
Tactic:
. intro hy
  rw [Set.mem_setOf_eq, Set.mem_Ioo] at hy
  obtain ⟨n, hn⟩ := exists_nat_gt (1 / dist x y)
  simp
  use n
  rw [sdef]
  simp
  constructor
  . rw [inv_lt, inv_eq_one_div]
    apply lt_trans hn
    linarith
    linarith
    exact hy.1
  . exact hy.2
Proof state after:
case h.mpr
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
s : ℕ → Set ℝ := fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
sdef : s = fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
y : ℝ
⊢ y ∈ ⋃ n, s n → y ∈ {y | dist x y ∈ Set.Ioo 0 1}
Theorem: le_CarlesonOperatorReal'
Proof state before:
case h.mpr
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
s : ℕ → Set ℝ := fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
sdef : s = fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
y : ℝ
⊢ y ∈ ⋃ n, s n → y ∈ {y | dist x y ∈ Set.Ioo 0 1}
Tactic:
. intro hy
  simp at hy
  rcases hy with ⟨n, hn⟩
  rw [sdef] at hn
  simp at hn
  constructor
  . apply lt_trans' hn.1
    norm_num
    linarith
  . exact hn.2
Proof state after:
no goals
Theorem: le_CarlesonOperatorReal'
Proof state before:
case h.mp
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
s : ℕ → Set ℝ := fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
sdef : s = fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
y : ℝ
⊢ y ∈ {y | dist x y ∈ Set.Ioo 0 1} → y ∈ ⋃ n, s n
Tactic:
intro hy
Proof state after:
case h.mp
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
s : ℕ → Set ℝ := fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
sdef : s = fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
y : ℝ
hy : y ∈ {y | dist x y ∈ Set.Ioo 0 1}
⊢ y ∈ ⋃ n, s n
Theorem: le_CarlesonOperatorReal'
Proof state before:
case h.mp
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
s : ℕ → Set ℝ := fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
sdef : s = fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
y : ℝ
hy : y ∈ {y | dist x y ∈ Set.Ioo 0 1}
⊢ y ∈ ⋃ n, s n
Tactic:
rw [Set.mem_setOf_eq, Set.mem_Ioo] at hy
Proof state after:
case h.mp
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
s : ℕ → Set ℝ := fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
sdef : s = fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
y : ℝ
hy : 0 < dist x y ∧ dist x y < 1
⊢ y ∈ ⋃ n, s n
Theorem: le_CarlesonOperatorReal'
Proof state before:
case h.mp
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
s : ℕ → Set ℝ := fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
sdef : s = fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
y : ℝ
hy : 0 < dist x y ∧ dist x y < 1
⊢ y ∈ ⋃ n, s n
Tactic:
obtain ⟨n, hn⟩ := exists_nat_gt (1 / dist x y)
Proof state after:
case h.mp.intro
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
s : ℕ → Set ℝ := fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
sdef : s = fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
y : ℝ
hy : 0 < dist x y ∧ dist x y < 1
n : ℕ
hn : 1 / dist x y < ↑n
⊢ y ∈ ⋃ n, s n
Theorem: le_CarlesonOperatorReal'
Proof state before:
case h.mp.intro
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
s : ℕ → Set ℝ := fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
sdef : s = fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
y : ℝ
hy : 0 < dist x y ∧ dist x y < 1
n : ℕ
hn : 1 / dist x y < ↑n
⊢ y ∈ ⋃ n, s n
Tactic:
simp
Proof state after:
case h.mp.intro
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
s : ℕ → Set ℝ := fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
sdef : s = fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
y : ℝ
hy : 0 < dist x y ∧ dist x y < 1
n : ℕ
hn : 1 / dist x y < ↑n
⊢ ∃ i, y ∈ s i
Theorem: le_CarlesonOperatorReal'
Proof state before:
case h.mp.intro
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
s : ℕ → Set ℝ := fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
sdef : s = fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
y : ℝ
hy : 0 < dist x y ∧ dist x y < 1
n : ℕ
hn : 1 / dist x y < ↑n
⊢ ∃ i, y ∈ s i
Tactic:
use n
Proof state after:
case h
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
s : ℕ → Set ℝ := fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
sdef : s = fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
y : ℝ
hy : 0 < dist x y ∧ dist x y < 1
n : ℕ
hn : 1 / dist x y < ↑n
⊢ y ∈ s n
Theorem: le_CarlesonOperatorReal'
Proof state before:
case h
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
s : ℕ → Set ℝ := fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
sdef : s = fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
y : ℝ
hy : 0 < dist x y ∧ dist x y < 1
n : ℕ
hn : 1 / dist x y < ↑n
⊢ y ∈ s n
Tactic:
rw [sdef]
Proof state after:
case h
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
s : ℕ → Set ℝ := fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
sdef : s = fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
y : ℝ
hy : 0 < dist x y ∧ dist x y < 1
n : ℕ
hn : 1 / dist x y < ↑n
⊢ y ∈ (fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}) n
Theorem: le_CarlesonOperatorReal'
Proof state before:
case h
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
s : ℕ → Set ℝ := fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
sdef : s = fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
y : ℝ
hy : 0 < dist x y ∧ dist x y < 1
n : ℕ
hn : 1 / dist x y < ↑n
⊢ y ∈ (fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}) n
Tactic:
simp
Proof state after:
case h
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
s : ℕ → Set ℝ := fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
sdef : s = fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
y : ℝ
hy : 0 < dist x y ∧ dist x y < 1
n : ℕ
hn : 1 / dist x y < ↑n
⊢ (↑n + 2)⁻¹ < dist x y ∧ dist x y < 1
Theorem: le_CarlesonOperatorReal'
Proof state before:
case h
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
s : ℕ → Set ℝ := fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
sdef : s = fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
y : ℝ
hy : 0 < dist x y ∧ dist x y < 1
n : ℕ
hn : 1 / dist x y < ↑n
⊢ (↑n + 2)⁻¹ < dist x y ∧ dist x y < 1
Tactic:
constructor
Proof state after:
case h.left
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
s : ℕ → Set ℝ := fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
sdef : s = fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
y : ℝ
hy : 0 < dist x y ∧ dist x y < 1
n : ℕ
hn : 1 / dist x y < ↑n
⊢ (↑n + 2)⁻¹ < dist x y

case h.right
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
s : ℕ → Set ℝ := fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
sdef : s = fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
y : ℝ
hy : 0 < dist x y ∧ dist x y < 1
n : ℕ
hn : 1 / dist x y < ↑n
⊢ dist x y < 1
Theorem: le_CarlesonOperatorReal'
Proof state before:
case h.left
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
s : ℕ → Set ℝ := fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
sdef : s = fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
y : ℝ
hy : 0 < dist x y ∧ dist x y < 1
n : ℕ
hn : 1 / dist x y < ↑n
⊢ (↑n + 2)⁻¹ < dist x y

case h.right
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
s : ℕ → Set ℝ := fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
sdef : s = fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
y : ℝ
hy : 0 < dist x y ∧ dist x y < 1
n : ℕ
hn : 1 / dist x y < ↑n
⊢ dist x y < 1
Tactic:
. rw [inv_lt, inv_eq_one_div]
  apply lt_trans hn
  linarith
  linarith
  exact hy.1
Proof state after:
case h.right
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
s : ℕ → Set ℝ := fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
sdef : s = fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
y : ℝ
hy : 0 < dist x y ∧ dist x y < 1
n : ℕ
hn : 1 / dist x y < ↑n
⊢ dist x y < 1
Theorem: le_CarlesonOperatorReal'
Proof state before:
case h.right
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
s : ℕ → Set ℝ := fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
sdef : s = fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
y : ℝ
hy : 0 < dist x y ∧ dist x y < 1
n : ℕ
hn : 1 / dist x y < ↑n
⊢ dist x y < 1
Tactic:
. exact hy.2
Proof state after:
no goals
Theorem: le_CarlesonOperatorReal'
Proof state before:
case h.left
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
s : ℕ → Set ℝ := fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
sdef : s = fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
y : ℝ
hy : 0 < dist x y ∧ dist x y < 1
n : ℕ
hn : 1 / dist x y < ↑n
⊢ (↑n + 2)⁻¹ < dist x y
Tactic:
rw [inv_lt, inv_eq_one_div]
Proof state after:
case h.left
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
s : ℕ → Set ℝ := fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
sdef : s = fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
y : ℝ
hy : 0 < dist x y ∧ dist x y < 1
n : ℕ
hn : 1 / dist x y < ↑n
⊢ 1 / dist x y < ↑n + 2

case h.left.ha
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
s : ℕ → Set ℝ := fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
sdef : s = fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
y : ℝ
hy : 0 < dist x y ∧ dist x y < 1
n : ℕ
hn : 1 / dist x y < ↑n
⊢ 0 < ↑n + 2

case h.left.hb
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
s : ℕ → Set ℝ := fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
sdef : s = fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
y : ℝ
hy : 0 < dist x y ∧ dist x y < 1
n : ℕ
hn : 1 / dist x y < ↑n
⊢ 0 < dist x y
Theorem: le_CarlesonOperatorReal'
Proof state before:
case h.left
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
s : ℕ → Set ℝ := fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
sdef : s = fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
y : ℝ
hy : 0 < dist x y ∧ dist x y < 1
n : ℕ
hn : 1 / dist x y < ↑n
⊢ 1 / dist x y < ↑n + 2

case h.left.ha
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
s : ℕ → Set ℝ := fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
sdef : s = fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
y : ℝ
hy : 0 < dist x y ∧ dist x y < 1
n : ℕ
hn : 1 / dist x y < ↑n
⊢ 0 < ↑n + 2

case h.left.hb
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
s : ℕ → Set ℝ := fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
sdef : s = fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
y : ℝ
hy : 0 < dist x y ∧ dist x y < 1
n : ℕ
hn : 1 / dist x y < ↑n
⊢ 0 < dist x y
Tactic:
apply lt_trans hn
Proof state after:
case h.left
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
s : ℕ → Set ℝ := fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
sdef : s = fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
y : ℝ
hy : 0 < dist x y ∧ dist x y < 1
n : ℕ
hn : 1 / dist x y < ↑n
⊢ ↑n < ↑n + 2

case h.left.ha
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
s : ℕ → Set ℝ := fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
sdef : s = fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
y : ℝ
hy : 0 < dist x y ∧ dist x y < 1
n : ℕ
hn : 1 / dist x y < ↑n
⊢ 0 < ↑n + 2

case h.left.hb
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
s : ℕ → Set ℝ := fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
sdef : s = fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
y : ℝ
hy : 0 < dist x y ∧ dist x y < 1
n : ℕ
hn : 1 / dist x y < ↑n
⊢ 0 < dist x y
Theorem: le_CarlesonOperatorReal'
Proof state before:
case h.left
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
s : ℕ → Set ℝ := fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
sdef : s = fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
y : ℝ
hy : 0 < dist x y ∧ dist x y < 1
n : ℕ
hn : 1 / dist x y < ↑n
⊢ ↑n < ↑n + 2

case h.left.ha
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
s : ℕ → Set ℝ := fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
sdef : s = fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
y : ℝ
hy : 0 < dist x y ∧ dist x y < 1
n : ℕ
hn : 1 / dist x y < ↑n
⊢ 0 < ↑n + 2

case h.left.hb
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
s : ℕ → Set ℝ := fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
sdef : s = fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
y : ℝ
hy : 0 < dist x y ∧ dist x y < 1
n : ℕ
hn : 1 / dist x y < ↑n
⊢ 0 < dist x y
Tactic:
linarith
Proof state after:
case h.left.ha
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
s : ℕ → Set ℝ := fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
sdef : s = fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
y : ℝ
hy : 0 < dist x y ∧ dist x y < 1
n : ℕ
hn : 1 / dist x y < ↑n
⊢ 0 < ↑n + 2

case h.left.hb
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
s : ℕ → Set ℝ := fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
sdef : s = fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
y : ℝ
hy : 0 < dist x y ∧ dist x y < 1
n : ℕ
hn : 1 / dist x y < ↑n
⊢ 0 < dist x y