internlm/Lean-Github huggingface dataset:
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:
set R' := (c + 2 * R * |(n : ℝ) - m|) / (4 * |(n : ℝ) - m|) with R'def
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
R' : ℝ := (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
R'def : R' = (c + 2 * R * |↑n - ↑m|) / (4 * |↑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
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|)
⊢ c < ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
Tactic:
have hR' : 0 ≤ R' ∧ R' < R := by
  rw [R'def]
  constructor
  . positivity
  calc (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
    _ < (2 * R * |↑n - ↑m| + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|) := by
      gcongr
    _ = R := by
      ring_nf
      rw [mul_assoc, mul_inv_cancel norm_n_sub_m_pos.ne.symm, mul_one]
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
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
⊢ 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
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
⊢ c < ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
Tactic:
let y := (x - R', x + R')
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
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 < ⨆ 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
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 < ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
Tactic:
calc c
  _ = c / 2 + c / 2 := by ring
  _ < c / 2 + (2 * R * |↑n - ↑m|) / 2 := by
    gcongr
  _ = 2 * R' * |↑n - ↑m| := by
    rw [R'def]
    ring_nf
    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]
    ring
  _ ≤ ‖(↑n - ↑m) * (y.1 - x) - (↑n - ↑m) * (y.2 - x)‖ := by
    simp
    rw [sub_eq_add_neg (-((n - m) * R')), ←neg_add, abs_neg, ←two_mul, abs_mul, abs_mul, mul_comm |(n : ℝ) - m|, mul_assoc]
    simp
    gcongr
    apply le_abs_self
  _ ≤ ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖ := by
    apply ConditionallyCompleteLattice.le_biSup
    . convert bddAbove_localOscillation (Metric.ball x R) (θ n) (θ m)
      apply norm_integer_linear_eq.symm
    . 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 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)‖
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:
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
⊢ 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)‖
Tactic:
rw [localOscillation]
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
⊢ ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ =
    ⨆ 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:
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
⊢ ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
Tactic:
congr
Proof state after:
case e_s
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
⊢ (fun z => ⨆ (_ : z ∈ Metric.ball x R ×ˢ Metric.ball x R), ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖) = fun z =>
    ⨆ (_ : 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 e_s
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
⊢ (fun z => ⨆ (_ : z ∈ Metric.ball x R ×ˢ Metric.ball x R), ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖) = fun z =>
    ⨆ (_ : z ∈ Metric.ball x R ×ˢ Metric.ball x R), ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
Tactic:
ext z
Proof state after:
case e_s.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
z : ℝ × ℝ
⊢ ⨆ (_ : z ∈ Metric.ball x R ×ˢ Metric.ball x R), ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ =
    ⨆ (_ : 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 e_s.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
z : ℝ × ℝ
⊢ ⨆ (_ : z ∈ Metric.ball x R ×ˢ Metric.ball x R), ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ =
    ⨆ (_ : z ∈ Metric.ball x R ×ˢ Metric.ball x R), ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
Tactic:
congr
Proof state after:
case e_s.h.e_s
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
z : ℝ × ℝ
⊢ (fun h => ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖) = fun h => ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
Theorem: localOscillation_of_integer_linear
Proof state before:
case e_s.h.e_s
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
z : ℝ × ℝ
⊢ (fun h => ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖) = fun h => ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
Tactic:
rw [norm_integer_linear_eq]
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|)
⊢ 0 ≤ R' ∧ R' < R
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|)
⊢ 0 ≤ (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|) ∧ (c + 2 * R * |↑n - ↑m|) / (4 * |↑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|)
⊢ 0 ≤ (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|) ∧ (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|) < R
Tactic:
constructor
Proof state after:
case left
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|)
⊢ 0 ≤ (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)

case right
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|)
⊢ (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|) < R
Theorem: localOscillation_of_integer_linear
Proof state before:
case left
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|)
⊢ 0 ≤ (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)

case right
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|)
⊢ (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|) < R
Tactic:
. positivity
Proof state after:
case right
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|)
⊢ (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|) < R
Theorem: localOscillation_of_integer_linear
Proof state before:
case right
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|)
⊢ (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|) < R
Tactic:
calc (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
  _ < (2 * R * |↑n - ↑m| + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|) := by
    gcongr
  _ = R := by
    ring_nf
    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:
case left
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|)
⊢ 0 ≤ (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
Tactic:
positivity
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|)
⊢ (c + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|) < (2 * R * |↑n - ↑m| + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|)
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|)
⊢ (2 * R * |↑n - ↑m| + 2 * R * |↑n - ↑m|) / (4 * |↑n - ↑m|) = R
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|)
⊢ R * |↑n - ↑m| * |↑n - ↑m|⁻¹ = R