internlm/Lean-Github huggingface dataset:
Theorem: localOscillation_of_integer_linear
Proof state before:
case hS.hS
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)‖
z : ℝ × ℝ
⊢ z ∈ Metric.ball x R ×ˢ Metric.ball x R → ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖ ≤ 2 * R * |↑n - ↑m|
Tactic:
intro hz
Proof state after:
case hS.hS
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)‖
z : ℝ × ℝ
hz : z ∈ Metric.ball x R ×ˢ Metric.ball x R
⊢ ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖ ≤ 2 * R * |↑n - ↑m|
Theorem: localOscillation_of_integer_linear
Proof state before:
case hS.hS
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)‖
z : ℝ × ℝ
hz : z ∈ Metric.ball x R ×ˢ Metric.ball x R
⊢ ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖ ≤ 2 * R * |↑n - ↑m|
Tactic:
simp at hz
Proof state after:
case hS.hS
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)‖
z : ℝ × ℝ
hz : dist z.1 x < R ∧ dist z.2 x < R
⊢ ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖ ≤ 2 * R * |↑n - ↑m|
Theorem: localOscillation_of_integer_linear
Proof state before:
case hS.hS
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)‖
z : ℝ × ℝ
hz : dist z.1 x < R ∧ dist z.2 x < R
⊢ ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖ ≤ 2 * R * |↑n - ↑m|
Tactic:
rw [Real.dist_eq, Real.dist_eq] at hz
Proof state after:
case hS.hS
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)‖
z : ℝ × ℝ
hz : |z.1 - x| < R ∧ |z.2 - x| < R
⊢ ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖ ≤ 2 * R * |↑n - ↑m|
Theorem: localOscillation_of_integer_linear
Proof state before:
case hS.hS
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)‖
z : ℝ × ℝ
hz : |z.1 - x| < R ∧ |z.2 - x| < R
⊢ ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖ ≤ 2 * R * |↑n - ↑m|
Tactic:
rw [Real.norm_eq_abs]
Proof state after:
case hS.hS
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)‖
z : ℝ × ℝ
hz : |z.1 - x| < R ∧ |z.2 - x| < R
⊢ |(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)| ≤ 2 * R * |↑n - ↑m|
Theorem: localOscillation_of_integer_linear
Proof state before:
case hS.hS
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)‖
z : ℝ × ℝ
hz : |z.1 - x| < R ∧ |z.2 - x| < R
⊢ |(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)| ≤ 2 * R * |↑n - ↑m|
Tactic:
calc |(n - m) * (z.1 - x) - (n - m) * (z.2 - x)|
_ ≤ |(n - m) * (z.1 - x)| + |(n - m) * (z.2 - x)| := by apply abs_sub
_ = |↑n - ↑m| * |z.1 - x| + |↑n - ↑m| * |z.2 - x| := by congr <;> apply abs_mul
_ ≤ |↑n - ↑m| * R + |↑n - ↑m| * R := by gcongr; linarith [hz.1]; linarith [hz.2]
_ = 2 * R * |↑n - ↑m| := by 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)‖
z : ℝ × ℝ
hz : |z.1 - x| < R ∧ |z.2 - x| < R
⊢ |(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)| ≤ |(↑n - ↑m) * (z.1 - x)| + |(↑n - ↑m) * (z.2 - x)|
Tactic:
apply abs_sub
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)‖
z : ℝ × ℝ
hz : |z.1 - x| < R ∧ |z.2 - x| < R
⊢ |(↑n - ↑m) * (z.1 - x)| + |(↑n - ↑m) * (z.2 - x)| = |↑n - ↑m| * |z.1 - x| + |↑n - ↑m| * |z.2 - x|
Tactic:
congr <;> apply abs_mul
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)‖
z : ℝ × ℝ
hz : |z.1 - x| < R ∧ |z.2 - x| < R
⊢ |↑n - ↑m| * |z.1 - x| + |↑n - ↑m| * |z.2 - x| ≤ |↑n - ↑m| * R + |↑n - ↑m| * R
Tactic:
gcongr
Proof state after:
case h₁.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)‖
z : ℝ × ℝ
hz : |z.1 - x| < R ∧ |z.2 - x| < R
⊢ |z.1 - x| ≤ R

case h₂.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)‖
z : ℝ × ℝ
hz : |z.1 - x| < R ∧ |z.2 - x| < R
⊢ |z.2 - x| ≤ R
Theorem: localOscillation_of_integer_linear
Proof state before:
case h₁.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)‖
z : ℝ × ℝ
hz : |z.1 - x| < R ∧ |z.2 - x| < R
⊢ |z.1 - x| ≤ R

case h₂.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)‖
z : ℝ × ℝ
hz : |z.1 - x| < R ∧ |z.2 - x| < R
⊢ |z.2 - x| ≤ R
Tactic:
linarith [hz.1]
Proof state after:
case h₂.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)‖
z : ℝ × ℝ
hz : |z.1 - x| < R ∧ |z.2 - x| < R
⊢ |z.2 - x| ≤ R
Theorem: localOscillation_of_integer_linear
Proof state before:
case h₂.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)‖
z : ℝ × ℝ
hz : |z.1 - x| < R ∧ |z.2 - x| < R
⊢ |z.2 - x| ≤ R
Tactic:
linarith [hz.2]
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)‖
z : ℝ × ℝ
hz : |z.1 - x| < R ∧ |z.2 - x| < R
⊢ |↑n - ↑m| * R + |↑n - ↑m| * R = 2 * R * |↑n - ↑m|
Tactic:
ring
Proof state after:
no goals
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)‖
⊢ 0 ≤ 2 * R * |↑n - ↑m|
Tactic:
apply mul_nonneg
Proof state after:
case ha.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)‖
⊢ 0 ≤ 2 * R

case ha.hb
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)‖
⊢ 0 ≤ |↑n - ↑m|
Theorem: localOscillation_of_integer_linear
Proof state before:
case ha.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)‖
⊢ 0 ≤ 2 * R

case ha.hb
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)‖
⊢ 0 ≤ |↑n - ↑m|
Tactic:
linarith
Proof state after:
case ha.hb
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)‖
⊢ 0 ≤ |↑n - ↑m|
Theorem: localOscillation_of_integer_linear
Proof state before:
case ha.hb
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)‖
⊢ 0 ≤ |↑n - ↑m|
Tactic:
apply abs_nonneg
Proof state after:
no goals
Theorem: localOscillation_of_integer_linear
Proof state before:
case neg.a
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)‖
⊢ 2 * R * |↑n - ↑m| ≤ ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
Tactic:
apply le_of_forall_lt
Proof state after:
case neg.a.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 < 2 * R * |↑n - ↑m|, c < ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
Theorem: localOscillation_of_integer_linear
Proof state before:
case neg.a.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 < 2 * R * |↑n - ↑m|, c < ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
Tactic:
intro c hc
Proof state after:
case neg.a.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|
⊢ c < ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
Theorem: localOscillation_of_integer_linear
Proof state before:
case neg.a.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|
⊢ c < ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
Tactic:
have := fact_isCompact_ball x R
Proof state after:
case neg.a.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 < ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
Theorem: localOscillation_of_integer_linear
Proof state before:
case neg.a.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 < ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
Tactic:
by_cases c_nonneg : 0 > c
Proof state after:
case pos
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
⊢ c < ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖

case neg
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
⊢ c < ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
Theorem: localOscillation_of_integer_linear
Proof state before:
case pos
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
⊢ c < ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖

case neg
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
⊢ c < ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
Tactic:
. calc c
    _ < 0 := c_nonneg
    _ ≤ @dist (withLocalOscillation (Metric.ball x R)) PseudoMetricSpace.toDist (θ n) (θ m) := dist_nonneg
    _ = localOscillation (Metric.ball x R) (θ n) (θ m) := rfl
    _ = ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖ := by
      rw [localOscillation]
      congr
      ext z
      congr
      rw [norm_integer_linear_eq]
Proof state after:
case neg
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
⊢ c < ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
Theorem: localOscillation_of_integer_linear
Proof state before:
case neg
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
⊢ c < ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
Tactic:
push_neg at c_nonneg
Proof state after:
case neg
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
⊢ c < ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖