internlm/Lean-Github huggingface dataset:
Theorem: localOscillation_of_integer_linear
Proof state before:
case ha
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
c : ℝ
hc : c < 2 * R * |↑n - ↑m|
this : Fact (Bornology.IsBounded (Metric.ball x R))
c_nonneg : 0 ≤ c
R' : ℝ := (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
R'def : R' = (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
hR' : 0 ≤ R' ∧ R' < R
y : ℝ × ℝ := (x - R', x + R')
⊢ ∃ i ∈ Metric.ball x R ×ˢ Metric.ball x R,
    ‖(↑n - ↑m) * (i.1 - x) - (↑n - ↑m) * (i.2 - x)‖ = ‖(↑n - ↑m) * (y.1 - x) - (↑n - ↑m) * (y.2 - x)‖
Tactic:
use y
Proof state after:
case h
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
c : ℝ
hc : c < 2 * R * |↑n - ↑m|
this : Fact (Bornology.IsBounded (Metric.ball x R))
c_nonneg : 0 ≤ c
R' : ℝ := (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
R'def : R' = (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
hR' : 0 ≤ R' ∧ R' < R
y : ℝ × ℝ := (x - R', x + R')
⊢ y ∈ Metric.ball x R ×ˢ Metric.ball x R ∧
    ‖(↑n - ↑m) * (y.1 - x) - (↑n - ↑m) * (y.2 - x)‖ = ‖(↑n - ↑m) * (y.1 - x) - (↑n - ↑m) * (y.2 - x)‖
Theorem: localOscillation_of_integer_linear
Proof state before:
case h
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
c : ℝ
hc : c < 2 * R * |↑n - ↑m|
this : Fact (Bornology.IsBounded (Metric.ball x R))
c_nonneg : 0 ≤ c
R' : ℝ := (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
R'def : R' = (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
hR' : 0 ≤ R' ∧ R' < R
y : ℝ × ℝ := (x - R', x + R')
⊢ y ∈ Metric.ball x R ×ˢ Metric.ball x R ∧
    ‖(↑n - ↑m) * (y.1 - x) - (↑n - ↑m) * (y.2 - x)‖ = ‖(↑n - ↑m) * (y.1 - x) - (↑n - ↑m) * (y.2 - x)‖
Tactic:
simp
Proof state after:
case h
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
c : ℝ
hc : c < 2 * R * |↑n - ↑m|
this : Fact (Bornology.IsBounded (Metric.ball x R))
c_nonneg : 0 ≤ c
R' : ℝ := (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
R'def : R' = (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
hR' : 0 ≤ R' ∧ R' < R
y : ℝ × ℝ := (x - R', x + R')
⊢ |R'| < R
Theorem: localOscillation_of_integer_linear
Proof state before:
case h
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
c : ℝ
hc : c < 2 * R * |↑n - ↑m|
this : Fact (Bornology.IsBounded (Metric.ball x R))
c_nonneg : 0 ≤ c
R' : ℝ := (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
R'def : R' = (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
hR' : 0 ≤ R' ∧ R' < R
y : ℝ × ℝ := (x - R', x + R')
⊢ |R'| < R
Tactic:
rw [abs_of_nonneg]
Proof state after:
case h
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
c : ℝ
hc : c < 2 * R * |↑n - ↑m|
this : Fact (Bornology.IsBounded (Metric.ball x R))
c_nonneg : 0 ≤ c
R' : ℝ := (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
R'def : R' = (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
hR' : 0 ≤ R' ∧ R' < R
y : ℝ × ℝ := (x - R', x + R')
⊢ R' < R

case h
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
c : ℝ
hc : c < 2 * R * |↑n - ↑m|
this : Fact (Bornology.IsBounded (Metric.ball x R))
c_nonneg : 0 ≤ c
R' : ℝ := (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
R'def : R' = (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
hR' : 0 ≤ R' ∧ R' < R
y : ℝ × ℝ := (x - R', x + R')
⊢ 0 ≤ R'
Theorem: localOscillation_of_integer_linear
Proof state before:
case h
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
c : ℝ
hc : c < 2 * R * |↑n - ↑m|
this : Fact (Bornology.IsBounded (Metric.ball x R))
c_nonneg : 0 ≤ c
R' : ℝ := (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
R'def : R' = (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
hR' : 0 ≤ R' ∧ R' < R
y : ℝ × ℝ := (x - R', x + R')
⊢ R' < R

case h
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
c : ℝ
hc : c < 2 * R * |↑n - ↑m|
this : Fact (Bornology.IsBounded (Metric.ball x R))
c_nonneg : 0 ≤ c
R' : ℝ := (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
R'def : R' = (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
hR' : 0 ≤ R' ∧ R' < R
y : ℝ × ℝ := (x - R', x + R')
⊢ 0 ≤ R'
Tactic:
exact hR'.2
Proof state after:
case h
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
c : ℝ
hc : c < 2 * R * |↑n - ↑m|
this : Fact (Bornology.IsBounded (Metric.ball x R))
c_nonneg : 0 ≤ c
R' : ℝ := (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
R'def : R' = (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
hR' : 0 ≤ R' ∧ R' < R
y : ℝ × ℝ := (x - R', x + R')
⊢ 0 ≤ R'
Theorem: localOscillation_of_integer_linear
Proof state before:
case h
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
c : ℝ
hc : c < 2 * R * |↑n - ↑m|
this : Fact (Bornology.IsBounded (Metric.ball x R))
c_nonneg : 0 ≤ c
R' : ℝ := (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
R'def : R' = (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
hR' : 0 ≤ R' ∧ R' < R
y : ℝ × ℝ := (x - R', x + R')
⊢ 0 ≤ R'
Tactic:
exact hR'.1
Proof state after:
no goals
Theorem: bciSup_of_emptyset
Proof state before:
α : Type
inst✝¹ : ConditionallyCompleteLattice α
ι : Type
inst✝ : Nonempty ι
f : ι → α
⊢ ⨆ i ∈ ∅, f i = sSup ∅
Tactic:
rw [iSup]
Proof state after:
α : Type
inst✝¹ : ConditionallyCompleteLattice α
ι : Type
inst✝ : Nonempty ι
f : ι → α
⊢ sSup (Set.range fun i => ⨆ (_ : i ∈ ∅), f i) = sSup ∅
Theorem: bciSup_of_emptyset
Proof state before:
α : Type
inst✝¹ : ConditionallyCompleteLattice α
ι : Type
inst✝ : Nonempty ι
f : ι → α
⊢ sSup (Set.range fun i => ⨆ (_ : i ∈ ∅), f i) = sSup ∅
Tactic:
convert csSup_singleton _
Proof state after:
case h.e'_2.h.e'_3
α : Type
inst✝¹ : ConditionallyCompleteLattice α
ι : Type
inst✝ : Nonempty ι
f : ι → α
⊢ (Set.range fun i => ⨆ (_ : i ∈ ∅), f i) = {sSup ∅}
Theorem: bciSup_of_emptyset
Proof state before:
case h.e'_2.h.e'_3
α : Type
inst✝¹ : ConditionallyCompleteLattice α
ι : Type
inst✝ : Nonempty ι
f : ι → α
⊢ (Set.range fun i => ⨆ (_ : i ∈ ∅), f i) = {sSup ∅}
Tactic:
have : ∀ i : ι, IsEmpty (i ∈ (∅ : Set ι)) := by
  intro i
  simp
Proof state after:
case h.e'_2.h.e'_3
α : Type
inst✝¹ : ConditionallyCompleteLattice α
ι : Type
inst✝ : Nonempty ι
f : ι → α
this : ∀ (i : ι), IsEmpty (i ∈ ∅)
⊢ (Set.range fun i => ⨆ (_ : i ∈ ∅), f i) = {sSup ∅}
Theorem: bciSup_of_emptyset
Proof state before:
case h.e'_2.h.e'_3
α : Type
inst✝¹ : ConditionallyCompleteLattice α
ι : Type
inst✝ : Nonempty ι
f : ι → α
this : ∀ (i : ι), IsEmpty (i ∈ ∅)
⊢ (Set.range fun i => ⨆ (_ : i ∈ ∅), f i) = {sSup ∅}
Tactic:
have : (fun (i : ι) ↦ ⨆ (_ : i ∈ (∅ : Set ι)), f i) = fun i ↦ sSup ∅ := by
  ext i
  rw [iSup]
  congr
  rw [Set.range_eq_empty_iff]
  simp
Proof state after:
case h.e'_2.h.e'_3
α : Type
inst✝¹ : ConditionallyCompleteLattice α
ι : Type
inst✝ : Nonempty ι
f : ι → α
this✝ : ∀ (i : ι), IsEmpty (i ∈ ∅)
this : (fun i => ⨆ (_ : i ∈ ∅), f i) = fun i => sSup ∅
⊢ (Set.range fun i => ⨆ (_ : i ∈ ∅), f i) = {sSup ∅}
Theorem: bciSup_of_emptyset
Proof state before:
case h.e'_2.h.e'_3
α : Type
inst✝¹ : ConditionallyCompleteLattice α
ι : Type
inst✝ : Nonempty ι
f : ι → α
this✝ : ∀ (i : ι), IsEmpty (i ∈ ∅)
this : (fun i => ⨆ (_ : i ∈ ∅), f i) = fun i => sSup ∅
⊢ (Set.range fun i => ⨆ (_ : i ∈ ∅), f i) = {sSup ∅}
Tactic:
rw [this]
Proof state after:
case h.e'_2.h.e'_3
α : Type
inst✝¹ : ConditionallyCompleteLattice α
ι : Type
inst✝ : Nonempty ι
f : ι → α
this✝ : ∀ (i : ι), IsEmpty (i ∈ ∅)
this : (fun i => ⨆ (_ : i ∈ ∅), f i) = fun i => sSup ∅
⊢ (Set.range fun i => sSup ∅) = {sSup ∅}
Theorem: bciSup_of_emptyset
Proof state before:
case h.e'_2.h.e'_3
α : Type
inst✝¹ : ConditionallyCompleteLattice α
ι : Type
inst✝ : Nonempty ι
f : ι → α
this✝ : ∀ (i : ι), IsEmpty (i ∈ ∅)
this : (fun i => ⨆ (_ : i ∈ ∅), f i) = fun i => sSup ∅
⊢ (Set.range fun i => sSup ∅) = {sSup ∅}
Tactic:
apply Set.range_const
Proof state after:
no goals
Theorem: bciSup_of_emptyset
Proof state before:
α : Type
inst✝¹ : ConditionallyCompleteLattice α
ι : Type
inst✝ : Nonempty ι
f : ι → α
⊢ ∀ (i : ι), IsEmpty (i ∈ ∅)
Tactic:
intro i
Proof state after:
α : Type
inst✝¹ : ConditionallyCompleteLattice α
ι : Type
inst✝ : Nonempty ι
f : ι → α
i : ι
⊢ IsEmpty (i ∈ ∅)
Theorem: bciSup_of_emptyset
Proof state before:
α : Type
inst✝¹ : ConditionallyCompleteLattice α
ι : Type
inst✝ : Nonempty ι
f : ι → α
i : ι
⊢ IsEmpty (i ∈ ∅)
Tactic:
simp
Proof state after:
no goals
Theorem: bciSup_of_emptyset
Proof state before:
α : Type
inst✝¹ : ConditionallyCompleteLattice α
ι : Type
inst✝ : Nonempty ι
f : ι → α
this : ∀ (i : ι), IsEmpty (i ∈ ∅)
⊢ (fun i => ⨆ (_ : i ∈ ∅), f i) = fun i => sSup ∅
Tactic:
ext i
Proof state after:
case h
α : Type
inst✝¹ : ConditionallyCompleteLattice α
ι : Type
inst✝ : Nonempty ι
f : ι → α
this : ∀ (i : ι), IsEmpty (i ∈ ∅)
i : ι
⊢ ⨆ (_ : i ∈ ∅), f i = sSup ∅
Theorem: bciSup_of_emptyset
Proof state before:
case h
α : Type
inst✝¹ : ConditionallyCompleteLattice α
ι : Type
inst✝ : Nonempty ι
f : ι → α
this : ∀ (i : ι), IsEmpty (i ∈ ∅)
i : ι
⊢ ⨆ (_ : i ∈ ∅), f i = sSup ∅
Tactic:
rw [iSup]
Proof state after:
case h
α : Type
inst✝¹ : ConditionallyCompleteLattice α
ι : Type
inst✝ : Nonempty ι
f : ι → α
this : ∀ (i : ι), IsEmpty (i ∈ ∅)
i : ι
⊢ sSup (Set.range fun x => f i) = sSup ∅
Theorem: bciSup_of_emptyset
Proof state before:
case h
α : Type
inst✝¹ : ConditionallyCompleteLattice α
ι : Type
inst✝ : Nonempty ι
f : ι → α
this : ∀ (i : ι), IsEmpty (i ∈ ∅)
i : ι
⊢ sSup (Set.range fun x => f i) = sSup ∅
Tactic:
congr
Proof state after:
case h.e_a
α : Type
inst✝¹ : ConditionallyCompleteLattice α
ι : Type
inst✝ : Nonempty ι
f : ι → α
this : ∀ (i : ι), IsEmpty (i ∈ ∅)
i : ι
⊢ (Set.range fun x => f i) = ∅
Theorem: bciSup_of_emptyset
Proof state before:
case h.e_a
α : Type
inst✝¹ : ConditionallyCompleteLattice α
ι : Type
inst✝ : Nonempty ι
f : ι → α
this : ∀ (i : ι), IsEmpty (i ∈ ∅)
i : ι
⊢ (Set.range fun x => f i) = ∅
Tactic:
rw [Set.range_eq_empty_iff]
Proof state after:
case h.e_a
α : Type
inst✝¹ : ConditionallyCompleteLattice α
ι : Type
inst✝ : Nonempty ι
f : ι → α
this : ∀ (i : ι), IsEmpty (i ∈ ∅)
i : ι
⊢ IsEmpty (i ∈ ∅)
Theorem: bciSup_of_emptyset
Proof state before:
case h.e_a
α : Type
inst✝¹ : ConditionallyCompleteLattice α
ι : Type
inst✝ : Nonempty ι
f : ι → α
this : ∀ (i : ι), IsEmpty (i ∈ ∅)
i : ι
⊢ IsEmpty (i ∈ ∅)
Tactic:
simp
Proof state after:
no goals
Theorem: CarlesonOperatorReal'_le_CarlesonOperator'
Proof state before:
⊢ T' ≤ CarlesonOperator' K {x | ∃ n, θ n = x}
Tactic:
intro f x
Proof state after:
f : ℝ → ℂ
x : ℝ
⊢ T' f x ≤ CarlesonOperator' K {x | ∃ n, θ n = x} f x
Theorem: CarlesonOperatorReal'_le_CarlesonOperator'
Proof state before:
f : ℝ → ℂ
x : ℝ
⊢ T' f x ≤ CarlesonOperator' K {x | ∃ n, θ n = x} f x
Tactic:
rw [CarlesonOperator', CarlesonOperatorReal']
Proof state after:
f : ℝ → ℂ
x : ℝ
⊢ ⨆ n,
      ⨆ r,
        ⨆ (_ : 0 < r),
          ⨆ (_ : r < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊ ≤
    ⨆ Q ∈ {x | ∃ n, θ n = x},
      ⨆ R₁,
        ⨆ R₂,
          ⨆ (_ : 0 < R₁),
            ⨆ (_ : R₁ < R₂), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo R₁ R₂}, K x y * f y * (Complex.I * Q y).exp‖₊
Theorem: CarlesonOperatorReal'_le_CarlesonOperator'
Proof state before:
f : ℝ → ℂ
x : ℝ
⊢ ⨆ n,
      ⨆ r,
        ⨆ (_ : 0 < r),
          ⨆ (_ : r < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊ ≤
    ⨆ Q ∈ {x | ∃ n, θ n = x},
      ⨆ R₁,
        ⨆ R₂,
          ⨆ (_ : 0 < R₁),
            ⨆ (_ : R₁ < R₂), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo R₁ R₂}, K x y * f y * (Complex.I * Q y).exp‖₊
Tactic:
apply iSup_le
Proof state after:
case h
f : ℝ → ℂ
x : ℝ
⊢ ∀ (i : ℤ),
    ⨆ r,
        ⨆ (_ : 0 < r),
          ⨆ (_ : r < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑i * ↑y).exp‖₊ ≤
      ⨆ Q ∈ {x | ∃ n, θ n = x},
        ⨆ R₁,
          ⨆ R₂,
            ⨆ (_ : 0 < R₁),
              ⨆ (_ : R₁ < R₂), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo R₁ R₂}, K x y * f y * (Complex.I * Q y).exp‖₊
Theorem: CarlesonOperatorReal'_le_CarlesonOperator'
Proof state before:
case h
f : ℝ → ℂ
x : ℝ
⊢ ∀ (i : ℤ),
    ⨆ r,
        ⨆ (_ : 0 < r),
          ⨆ (_ : r < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑i * ↑y).exp‖₊ ≤
      ⨆ Q ∈ {x | ∃ n, θ n = x},
        ⨆ R₁,
          ⨆ R₂,
            ⨆ (_ : 0 < R₁),
              ⨆ (_ : R₁ < R₂), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo R₁ R₂}, K x y * f y * (Complex.I * Q y).exp‖₊
Tactic:
intro n
Proof state after:
case h
f : ℝ → ℂ
x : ℝ
n : ℤ
⊢ ⨆ r,
      ⨆ (_ : 0 < r),
        ⨆ (_ : r < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊ ≤
    ⨆ Q ∈ {x | ∃ n, θ n = x},
      ⨆ R₁,
        ⨆ R₂,
          ⨆ (_ : 0 < R₁),
            ⨆ (_ : R₁ < R₂), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo R₁ R₂}, K x y * f y * (Complex.I * Q y).exp‖₊
Theorem: CarlesonOperatorReal'_le_CarlesonOperator'
Proof state before:
case h
f : ℝ → ℂ
x : ℝ
n : ℤ
⊢ ⨆ r,
      ⨆ (_ : 0 < r),
        ⨆ (_ : r < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊ ≤
    ⨆ Q ∈ {x | ∃ n, θ n = x},
      ⨆ R₁,
        ⨆ R₂,
          ⨆ (_ : 0 < R₁),
            ⨆ (_ : R₁ < R₂), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo R₁ R₂}, K x y * f y * (Complex.I * Q y).exp‖₊
Tactic:
apply iSup_le
Proof state after:
case h.h
f : ℝ → ℂ
x : ℝ
n : ℤ
⊢ ∀ (i : ℝ),
    ⨆ (_ : 0 < i),
        ⨆ (_ : i < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo i 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊ ≤
      ⨆ Q ∈ {x | ∃ n, θ n = x},
        ⨆ R₁,
          ⨆ R₂,
            ⨆ (_ : 0 < R₁),
              ⨆ (_ : R₁ < R₂), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo R₁ R₂}, K x y * f y * (Complex.I * Q y).exp‖₊
Theorem: CarlesonOperatorReal'_le_CarlesonOperator'
Proof state before:
case h.h
f : ℝ → ℂ
x : ℝ
n : ℤ
⊢ ∀ (i : ℝ),
    ⨆ (_ : 0 < i),
        ⨆ (_ : i < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo i 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊ ≤
      ⨆ Q ∈ {x | ∃ n, θ n = x},
        ⨆ R₁,
          ⨆ R₂,
            ⨆ (_ : 0 < R₁),
              ⨆ (_ : R₁ < R₂), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo R₁ R₂}, K x y * f y * (Complex.I * Q y).exp‖₊
Tactic:
intro r
Proof state after:
case h.h
f : ℝ → ℂ
x : ℝ
n : ℤ
r : ℝ
⊢ ⨆ (_ : 0 < r), ⨆ (_ : r < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊ ≤
    ⨆ Q ∈ {x | ∃ n, θ n = x},
      ⨆ R₁,
        ⨆ R₂,
          ⨆ (_ : 0 < R₁),
            ⨆ (_ : R₁ < R₂), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo R₁ R₂}, K x y * f y * (Complex.I * Q y).exp‖₊
Theorem: CarlesonOperatorReal'_le_CarlesonOperator'
Proof state before:
case h.h
f : ℝ → ℂ
x : ℝ
n : ℤ
r : ℝ
⊢ ⨆ (_ : 0 < r), ⨆ (_ : r < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊ ≤
    ⨆ Q ∈ {x | ∃ n, θ n = x},
      ⨆ R₁,
        ⨆ R₂,
          ⨆ (_ : 0 < R₁),
            ⨆ (_ : R₁ < R₂), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo R₁ R₂}, K x y * f y * (Complex.I * Q y).exp‖₊
Tactic:
apply iSup_le
Proof state after:
case h.h.h
f : ℝ → ℂ
x : ℝ
n : ℤ
r : ℝ
⊢ 0 < r →
    ⨆ (_ : r < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊ ≤
      ⨆ Q ∈ {x | ∃ n, θ n = x},
        ⨆ R₁,
          ⨆ R₂,
            ⨆ (_ : 0 < R₁),
              ⨆ (_ : R₁ < R₂), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo R₁ R₂}, K x y * f y * (Complex.I * Q y).exp‖₊
Theorem: CarlesonOperatorReal'_le_CarlesonOperator'
Proof state before:
case h.h.h
f : ℝ → ℂ
x : ℝ
n : ℤ
r : ℝ
⊢ 0 < r →
    ⨆ (_ : r < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊ ≤
      ⨆ Q ∈ {x | ∃ n, θ n = x},
        ⨆ R₁,
          ⨆ R₂,
            ⨆ (_ : 0 < R₁),
              ⨆ (_ : R₁ < R₂), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo R₁ R₂}, K x y * f y * (Complex.I * Q y).exp‖₊
Tactic:
intro rpos
Proof state after:
case h.h.h
f : ℝ → ℂ
x : ℝ
n : ℤ
r : ℝ
rpos : 0 < r
⊢ ⨆ (_ : r < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊ ≤
    ⨆ Q ∈ {x | ∃ n, θ n = x},
      ⨆ R₁,
        ⨆ R₂,
          ⨆ (_ : 0 < R₁),
            ⨆ (_ : R₁ < R₂), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo R₁ R₂}, K x y * f y * (Complex.I * Q y).exp‖₊
Theorem: CarlesonOperatorReal'_le_CarlesonOperator'
Proof state before:
case h.h.h
f : ℝ → ℂ
x : ℝ
n : ℤ
r : ℝ
rpos : 0 < r
⊢ ⨆ (_ : r < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊ ≤
    ⨆ Q ∈ {x | ∃ n, θ n = x},
      ⨆ R₁,
        ⨆ R₂,
          ⨆ (_ : 0 < R₁),
            ⨆ (_ : R₁ < R₂), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo R₁ R₂}, K x y * f y * (Complex.I * Q y).exp‖₊
Tactic:
apply iSup_le
Proof state after:
case h.h.h.h
f : ℝ → ℂ
x : ℝ
n : ℤ
r : ℝ
rpos : 0 < r
⊢ r < 1 →
    ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊ ≤
      ⨆ Q ∈ {x | ∃ n, θ n = x},
        ⨆ R₁,
          ⨆ R₂,
            ⨆ (_ : 0 < R₁),
              ⨆ (_ : R₁ < R₂), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo R₁ R₂}, K x y * f y * (Complex.I * Q y).exp‖₊
Theorem: CarlesonOperatorReal'_le_CarlesonOperator'
Proof state before:
case h.h.h.h
f : ℝ → ℂ
x : ℝ
n : ℤ
r : ℝ
rpos : 0 < r
⊢ r < 1 →
    ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊ ≤
      ⨆ Q ∈ {x | ∃ n, θ n = x},
        ⨆ R₁,
          ⨆ R₂,
            ⨆ (_ : 0 < R₁),
              ⨆ (_ : R₁ < R₂), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo R₁ R₂}, K x y * f y * (Complex.I * Q y).exp‖₊
Tactic:
intro rle1
Proof state after:
case h.h.h.h
f : ℝ → ℂ
x : ℝ
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
⊢ ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊ ≤
    ⨆ Q ∈ {x | ∃ n, θ n = x},
      ⨆ R₁,
        ⨆ R₂,
          ⨆ (_ : 0 < R₁),
            ⨆ (_ : R₁ < R₂), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo R₁ R₂}, K x y * f y * (Complex.I * Q y).exp‖₊
Theorem: CarlesonOperatorReal'_le_CarlesonOperator'
Proof state before:
case h.h.h.h
f : ℝ → ℂ
x : ℝ
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
⊢ ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊ ≤
    ⨆ Q ∈ {x | ∃ n, θ n = x},
      ⨆ R₁,
        ⨆ R₂,
          ⨆ (_ : 0 < R₁),
            ⨆ (_ : R₁ < R₂), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo R₁ R₂}, K x y * f y * (Complex.I * Q y).exp‖₊
Tactic:
apply le_iSup₂_of_le (θ n) (by simp)
Proof state after:
case h.h.h.h
f : ℝ → ℂ
x : ℝ
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
⊢ ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊ ≤
    ⨆ R₁,
      ⨆ R₂,
        ⨆ (_ : 0 < R₁),
          ⨆ (_ : R₁ < R₂), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo R₁ R₂}, K x y * f y * (Complex.I * (θ n) y).exp‖₊
Theorem: CarlesonOperatorReal'_le_CarlesonOperator'
Proof state before:
case h.h.h.h
f : ℝ → ℂ
x : ℝ
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
⊢ ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊ ≤
    ⨆ R₁,
      ⨆ R₂,
        ⨆ (_ : 0 < R₁),
          ⨆ (_ : R₁ < R₂), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo R₁ R₂}, K x y * f y * (Complex.I * (θ n) y).exp‖₊
Tactic:
apply le_iSup₂_of_le r 1
Proof state after:
case h.h.h.h
f : ℝ → ℂ
x : ℝ
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
⊢ ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊ ≤
    ⨆ (_ : 0 < r), ⨆ (_ : r < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, K x y * f y * (Complex.I * (θ n) y).exp‖₊
Theorem: CarlesonOperatorReal'_le_CarlesonOperator'
Proof state before:
case h.h.h.h
f : ℝ → ℂ
x : ℝ
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
⊢ ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊ ≤
    ⨆ (_ : 0 < r), ⨆ (_ : r < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, K x y * f y * (Complex.I * (θ n) y).exp‖₊
Tactic:
apply le_iSup₂_of_le rpos rle1
Proof state after:
case h.h.h.h
f : ℝ → ℂ
x : ℝ
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
⊢ ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊ ≤
    ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, K x y * f y * (Complex.I * (θ n) y).exp‖₊
Theorem: CarlesonOperatorReal'_le_CarlesonOperator'
Proof state before:
case h.h.h.h
f : ℝ → ℂ
x : ℝ
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
⊢ ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊ ≤
    ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, K x y * f y * (Complex.I * (θ n) y).exp‖₊
Tactic:
apply le_of_eq
Proof state after:
case h.h.h.h.a
f : ℝ → ℂ
x : ℝ
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
⊢ ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊ =
    ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, K x y * f y * (Complex.I * (θ n) y).exp‖₊