internlm/Lean-Github huggingface dataset:
Theorem: localOscillation_of_integer_linear
Proof state before:
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|)
⊢ R * |↑n - ↑m| * |↑n - ↑m|⁻¹ = R
Tactic:
rw [mul_assoc, mul_inv_cancel norm_n_sub_m_pos.ne.symm, mul_one]
Proof state after:
no goals
Theorem: localOscillation_of_integer_linear
Proof state before:
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')
⊢ c = c / 2 + c / 2
Tactic:
ring
Proof state after:
no goals
Theorem: localOscillation_of_integer_linear
Proof state before:
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')
⊢ c / 2 + c / 2 < c / 2 + 2 * R * |↑n - ↑m| / 2
Tactic:
gcongr
Proof state after:
no goals
Theorem: localOscillation_of_integer_linear
Proof state before:
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')
⊢ c / 2 + 2 * R * |↑n - ↑m| / 2 = 2 * R' * |↑n - ↑m|
Tactic:
rw [R'def]
Proof state after:
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')
⊢ c / 2 + 2 * R * |↑n - ↑m| / 2 = 2 * ((c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)) * |↑n - ↑m|
Theorem: localOscillation_of_integer_linear
Proof state before:
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')
⊢ c / 2 + 2 * R * |↑n - ↑m| / 2 = 2 * ((c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)) * |↑n - ↑m|
Tactic:
ring_nf
Proof state after:
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')
⊢ c * (1 / 2) + R * |↑n - ↑m| = c * |↑n - ↑m| * |↑n - ↑m|⁻¹ * (1 / 2) + R * |↑n - ↑m| ^ 2 * |↑n - ↑m|⁻¹
Theorem: localOscillation_of_integer_linear
Proof state before:
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')
⊢ c * (1 / 2) + R * |↑n - ↑m| = c * |↑n - ↑m| * |↑n - ↑m|⁻¹ * (1 / 2) + R * |↑n - ↑m| ^ 2 * |↑n - ↑m|⁻¹
Tactic:
rw [pow_two, ←mul_assoc, mul_assoc c, mul_inv_cancel norm_n_sub_m_pos.ne.symm, mul_assoc (R * _), mul_inv_cancel norm_n_sub_m_pos.ne.symm]
Proof state after:
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')
⊢ c * (1 / 2) + R * |↑n - ↑m| = c * 1 * (1 / 2) + R * |↑n - ↑m| * 1
Theorem: localOscillation_of_integer_linear
Proof state before:
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')
⊢ c * (1 / 2) + R * |↑n - ↑m| = c * 1 * (1 / 2) + R * |↑n - ↑m| * 1
Tactic:
ring
Proof state after:
no goals
Theorem: localOscillation_of_integer_linear
Proof state before:
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')
⊢ 2 * R' * |↑n - ↑m| ≤ ‖(↑n - ↑m) * (y.1 - x) - (↑n - ↑m) * (y.2 - x)‖
Tactic:
simp
Proof state after:
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')
⊢ 2 * R' * |↑n - ↑m| ≤ |-((↑n - ↑m) * R') - (↑n - ↑m) * R'|
Theorem: localOscillation_of_integer_linear
Proof state before:
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')
⊢ 2 * R' * |↑n - ↑m| ≤ |-((↑n - ↑m) * R') - (↑n - ↑m) * R'|
Tactic:
rw [sub_eq_add_neg (-((n - m) * R')), ←neg_add, abs_neg, ←two_mul, abs_mul, abs_mul, mul_comm |(n : ℝ) - m|, mul_assoc]
Proof state after:
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')
⊢ 2 * (R' * |↑n - ↑m|) ≤ |2| * (|R'| * |↑n - ↑m|)
Theorem: localOscillation_of_integer_linear
Proof state before:
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')
⊢ 2 * (R' * |↑n - ↑m|) ≤ |2| * (|R'| * |↑n - ↑m|)
Tactic:
simp
Proof state after:
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' * |↑n - ↑m| ≤ |R'| * |↑n - ↑m|
Theorem: localOscillation_of_integer_linear
Proof state before:
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' * |↑n - ↑m| ≤ |R'| * |↑n - ↑m|
Tactic:
gcongr
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:
apply le_abs_self
Proof state after:
no goals
Theorem: localOscillation_of_integer_linear
Proof state before:
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')
⊢ ‖(↑n - ↑m) * (y.1 - x) - (↑n - ↑m) * (y.2 - x)‖ ≤
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
Tactic:
apply ConditionallyCompleteLattice.le_biSup
Proof state after:
case hfs
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')
⊢ BddAbove ((fun i => ‖(↑n - ↑m) * (i.1 - x) - (↑n - ↑m) * (i.2 - x)‖) '' Metric.ball x R ×ˢ Metric.ball x R)

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)‖
Theorem: localOscillation_of_integer_linear
Proof state before:
case hfs
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')
⊢ BddAbove ((fun i => ‖(↑n - ↑m) * (i.1 - x) - (↑n - ↑m) * (i.2 - x)‖) '' Metric.ball x R ×ˢ Metric.ball x R)

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:
. convert bddAbove_localOscillation (Metric.ball x R) (θ n) (θ m)
  apply norm_integer_linear_eq.symm
Proof state after:
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)‖
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
  simp
  rw [abs_of_nonneg]
  exact hR'.2
  exact hR'.1
Proof state after:
no goals
Theorem: localOscillation_of_integer_linear
Proof state before:
case hfs
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')
⊢ BddAbove ((fun i => ‖(↑n - ↑m) * (i.1 - x) - (↑n - ↑m) * (i.2 - x)‖) '' Metric.ball x R ×ˢ Metric.ball x R)
Tactic:
convert bddAbove_localOscillation (Metric.ball x R) (θ n) (θ m)
Proof state after:
case h.e'_3.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')
a✝¹ : ℝ × ℝ
a✝ : a✝¹ ∈ Metric.ball x R ×ˢ Metric.ball x R
⊢ ‖(↑n - ↑m) * (a✝¹.1 - x) - (↑n - ↑m) * (a✝¹.2 - x)‖ = ‖(θ n) a✝¹.1 - (θ m) a✝¹.1 - (θ n) a✝¹.2 + (θ m) a✝¹.2‖
Theorem: localOscillation_of_integer_linear
Proof state before:
case h.e'_3.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')
a✝¹ : ℝ × ℝ
a✝ : a✝¹ ∈ Metric.ball x R ×ˢ Metric.ball x R
⊢ ‖(↑n - ↑m) * (a✝¹.1 - x) - (↑n - ↑m) * (a✝¹.2 - x)‖ = ‖(θ n) a✝¹.1 - (θ m) a✝¹.1 - (θ n) a✝¹.2 + (θ m) a✝¹.2‖
Tactic:
apply norm_integer_linear_eq.symm
Proof state after:
no goals