internlm/Lean-Github huggingface dataset:
Theorem: lower_secant_bound'
Proof state before:
η : ℝ
ηpos : 0 < η
x : ℝ
le_abs_x : η ≤ x
abs_x_le : x ≤ 2 * Real.pi - η
x_nonneg : 0 ≤ x
x_le_pi : x ≤ Real.pi
h : Real.pi / 2 < x
⊢ 1 - x.cos ≤ √((1 - x.cos) ^ 2)
Tactic:
rw [Real.sqrt_sq_eq_abs]
Proof state after:
η : ℝ
ηpos : 0 < η
x : ℝ
le_abs_x : η ≤ x
abs_x_le : x ≤ 2 * Real.pi - η
x_nonneg : 0 ≤ x
x_le_pi : x ≤ Real.pi
h : Real.pi / 2 < x
⊢ 1 - x.cos ≤ |1 - x.cos|
Theorem: lower_secant_bound'
Proof state before:
η : ℝ
ηpos : 0 < η
x : ℝ
le_abs_x : η ≤ x
abs_x_le : x ≤ 2 * Real.pi - η
x_nonneg : 0 ≤ x
x_le_pi : x ≤ Real.pi
h : Real.pi / 2 < x
⊢ 1 - x.cos ≤ |1 - x.cos|
Tactic:
apply le_abs_self
Proof state after:
no goals
Theorem: lower_secant_bound'
Proof state before:
η : ℝ
ηpos : 0 < η
x : ℝ
le_abs_x : η ≤ x
abs_x_le : x ≤ 2 * Real.pi - η
x_nonneg : 0 ≤ x
x_le_pi : x ≤ Real.pi
h : Real.pi / 2 < x
⊢ √((1 - x.cos) ^ 2) ≤ ‖1 - (Complex.I * ↑x).exp‖
Tactic:
rw [mul_comm, Complex.exp_mul_I, Complex.norm_eq_abs, Complex.abs_eq_sqrt_sq_add_sq]
Proof state after:
η : ℝ
ηpos : 0 < η
x : ℝ
le_abs_x : η ≤ x
abs_x_le : x ≤ 2 * Real.pi - η
x_nonneg : 0 ≤ x
x_le_pi : x ≤ Real.pi
h : Real.pi / 2 < x
⊢ √((1 - x.cos) ^ 2) ≤
    √((1 - ((↑x).cos + (↑x).sin * Complex.I)).re ^ 2 + (1 - ((↑x).cos + (↑x).sin * Complex.I)).im ^ 2)
Theorem: lower_secant_bound'
Proof state before:
η : ℝ
ηpos : 0 < η
x : ℝ
le_abs_x : η ≤ x
abs_x_le : x ≤ 2 * Real.pi - η
x_nonneg : 0 ≤ x
x_le_pi : x ≤ Real.pi
h : Real.pi / 2 < x
⊢ √((1 - x.cos) ^ 2) ≤
    √((1 - ((↑x).cos + (↑x).sin * Complex.I)).re ^ 2 + (1 - ((↑x).cos + (↑x).sin * Complex.I)).im ^ 2)
Tactic:
simp
Proof state after:
η : ℝ
ηpos : 0 < η
x : ℝ
le_abs_x : η ≤ x
abs_x_le : x ≤ 2 * Real.pi - η
x_nonneg : 0 ≤ x
x_le_pi : x ≤ Real.pi
h : Real.pi / 2 < x
⊢ √((1 - x.cos) ^ 2) ≤ √((1 - (↑x).cos.re) ^ 2 + (↑x).sin.re ^ 2)
Theorem: lower_secant_bound'
Proof state before:
η : ℝ
ηpos : 0 < η
x : ℝ
le_abs_x : η ≤ x
abs_x_le : x ≤ 2 * Real.pi - η
x_nonneg : 0 ≤ x
x_le_pi : x ≤ Real.pi
h : Real.pi / 2 < x
⊢ √((1 - x.cos) ^ 2) ≤ √((1 - (↑x).cos.re) ^ 2 + (↑x).sin.re ^ 2)
Tactic:
rw [Complex.cos_ofReal_re, Complex.sin_ofReal_re]
Proof state after:
η : ℝ
ηpos : 0 < η
x : ℝ
le_abs_x : η ≤ x
abs_x_le : x ≤ 2 * Real.pi - η
x_nonneg : 0 ≤ x
x_le_pi : x ≤ Real.pi
h : Real.pi / 2 < x
⊢ √((1 - x.cos) ^ 2) ≤ √((1 - x.cos) ^ 2 + x.sin ^ 2)
Theorem: lower_secant_bound'
Proof state before:
η : ℝ
ηpos : 0 < η
x : ℝ
le_abs_x : η ≤ x
abs_x_le : x ≤ 2 * Real.pi - η
x_nonneg : 0 ≤ x
x_le_pi : x ≤ Real.pi
h : Real.pi / 2 < x
⊢ √((1 - x.cos) ^ 2) ≤ √((1 - x.cos) ^ 2 + x.sin ^ 2)
Tactic:
apply (Real.sqrt_le_sqrt_iff _).mpr
Proof state after:
η : ℝ
ηpos : 0 < η
x : ℝ
le_abs_x : η ≤ x
abs_x_le : x ≤ 2 * Real.pi - η
x_nonneg : 0 ≤ x
x_le_pi : x ≤ Real.pi
h : Real.pi / 2 < x
⊢ (1 - x.cos) ^ 2 ≤ (1 - x.cos) ^ 2 + x.sin ^ 2

η : ℝ
ηpos : 0 < η
x : ℝ
le_abs_x : η ≤ x
abs_x_le : x ≤ 2 * Real.pi - η
x_nonneg : 0 ≤ x
x_le_pi : x ≤ Real.pi
h : Real.pi / 2 < x
⊢ 0 ≤ (1 - x.cos) ^ 2 + x.sin ^ 2
Theorem: lower_secant_bound'
Proof state before:
η : ℝ
ηpos : 0 < η
x : ℝ
le_abs_x : η ≤ x
abs_x_le : x ≤ 2 * Real.pi - η
x_nonneg : 0 ≤ x
x_le_pi : x ≤ Real.pi
h : Real.pi / 2 < x
⊢ (1 - x.cos) ^ 2 ≤ (1 - x.cos) ^ 2 + x.sin ^ 2

η : ℝ
ηpos : 0 < η
x : ℝ
le_abs_x : η ≤ x
abs_x_le : x ≤ 2 * Real.pi - η
x_nonneg : 0 ≤ x
x_le_pi : x ≤ Real.pi
h : Real.pi / 2 < x
⊢ 0 ≤ (1 - x.cos) ^ 2 + x.sin ^ 2
Tactic:
. simp [pow_two_nonneg]
Proof state after:
η : ℝ
ηpos : 0 < η
x : ℝ
le_abs_x : η ≤ x
abs_x_le : x ≤ 2 * Real.pi - η
x_nonneg : 0 ≤ x
x_le_pi : x ≤ Real.pi
h : Real.pi / 2 < x
⊢ 0 ≤ (1 - x.cos) ^ 2 + x.sin ^ 2
Theorem: lower_secant_bound'
Proof state before:
η : ℝ
ηpos : 0 < η
x : ℝ
le_abs_x : η ≤ x
abs_x_le : x ≤ 2 * Real.pi - η
x_nonneg : 0 ≤ x
x_le_pi : x ≤ Real.pi
h : Real.pi / 2 < x
⊢ 0 ≤ (1 - x.cos) ^ 2 + x.sin ^ 2
Tactic:
. linarith [pow_two_nonneg (1 - Real.cos x), pow_two_nonneg (Real.sin x)]
Proof state after:
no goals
Theorem: lower_secant_bound'
Proof state before:
η : ℝ
ηpos : 0 < η
x : ℝ
le_abs_x : η ≤ x
abs_x_le : x ≤ 2 * Real.pi - η
x_nonneg : 0 ≤ x
x_le_pi : x ≤ Real.pi
h : Real.pi / 2 < x
⊢ (1 - x.cos) ^ 2 ≤ (1 - x.cos) ^ 2 + x.sin ^ 2
Tactic:
simp [pow_two_nonneg]
Proof state after:
no goals
Theorem: lower_secant_bound'
Proof state before:
η : ℝ
ηpos : 0 < η
x : ℝ
le_abs_x : η ≤ x
abs_x_le : x ≤ 2 * Real.pi - η
x_nonneg : 0 ≤ x
x_le_pi : x ≤ Real.pi
h : Real.pi / 2 < x
⊢ 0 ≤ (1 - x.cos) ^ 2 + x.sin ^ 2
Tactic:
linarith [pow_two_nonneg (1 - Real.cos x), pow_two_nonneg (Real.sin x)]
Proof state after:
no goals
Theorem: lower_secant_bound
Proof state before:
η x : ℝ
xIcc : x ∈ Set.Icc (-2 * Real.pi + η) (2 * Real.pi - η)
xAbs : η ≤ |x|
⊢ η / 2 ≤ Complex.abs (1 - (Complex.I * ↑x).exp)
Tactic:
by_cases ηpos : η < 0
Proof state after:
case pos
η x : ℝ
xIcc : x ∈ Set.Icc (-2 * Real.pi + η) (2 * Real.pi - η)
xAbs : η ≤ |x|
ηpos : η < 0
⊢ η / 2 ≤ Complex.abs (1 - (Complex.I * ↑x).exp)

case neg
η x : ℝ
xIcc : x ∈ Set.Icc (-2 * Real.pi + η) (2 * Real.pi - η)
xAbs : η ≤ |x|
ηpos : ¬η < 0
⊢ η / 2 ≤ Complex.abs (1 - (Complex.I * ↑x).exp)
Theorem: lower_secant_bound
Proof state before:
case pos
η x : ℝ
xIcc : x ∈ Set.Icc (-2 * Real.pi + η) (2 * Real.pi - η)
xAbs : η ≤ |x|
ηpos : η < 0
⊢ η / 2 ≤ Complex.abs (1 - (Complex.I * ↑x).exp)

case neg
η x : ℝ
xIcc : x ∈ Set.Icc (-2 * Real.pi + η) (2 * Real.pi - η)
xAbs : η ≤ |x|
ηpos : ¬η < 0
⊢ η / 2 ≤ Complex.abs (1 - (Complex.I * ↑x).exp)
Tactic:
. calc η / 2
  _ ≤ 0 := by linarith
  _ ≤ ‖1 - Complex.exp (Complex.I * x)‖ := by apply norm_nonneg
Proof state after:
case neg
η x : ℝ
xIcc : x ∈ Set.Icc (-2 * Real.pi + η) (2 * Real.pi - η)
xAbs : η ≤ |x|
ηpos : ¬η < 0
⊢ η / 2 ≤ Complex.abs (1 - (Complex.I * ↑x).exp)
Theorem: lower_secant_bound
Proof state before:
case neg
η x : ℝ
xIcc : x ∈ Set.Icc (-2 * Real.pi + η) (2 * Real.pi - η)
xAbs : η ≤ |x|
ηpos : ¬η < 0
⊢ η / 2 ≤ Complex.abs (1 - (Complex.I * ↑x).exp)
Tactic:
push_neg at ηpos
Proof state after:
case neg
η x : ℝ
xIcc : x ∈ Set.Icc (-2 * Real.pi + η) (2 * Real.pi - η)
xAbs : η ≤ |x|
ηpos : 0 ≤ η
⊢ η / 2 ≤ Complex.abs (1 - (Complex.I * ↑x).exp)
Theorem: lower_secant_bound
Proof state before:
case neg
η x : ℝ
xIcc : x ∈ Set.Icc (-2 * Real.pi + η) (2 * Real.pi - η)
xAbs : η ≤ |x|
ηpos : 0 ≤ η
⊢ η / 2 ≤ Complex.abs (1 - (Complex.I * ↑x).exp)
Tactic:
calc η / 2
_ ≤ (2 / Real.pi) * η := by
  ring_nf
  rw [mul_assoc]
  gcongr
  field_simp
  rw [div_le_div_iff (by norm_num) Real.pi_pos]
  linarith [Real.pi_le_four]
_ ≤ ‖1 - Complex.exp (Complex.I * x)‖ := by
  apply lower_secant_bound' xAbs
  rw [abs_le, neg_sub', sub_neg_eq_add, neg_mul_eq_neg_mul]
  exact xIcc
Proof state after:
no goals
Theorem: lower_secant_bound
Proof state before:
case pos
η x : ℝ
xIcc : x ∈ Set.Icc (-2 * Real.pi + η) (2 * Real.pi - η)
xAbs : η ≤ |x|
ηpos : η < 0
⊢ η / 2 ≤ Complex.abs (1 - (Complex.I * ↑x).exp)
Tactic:
calc η / 2
_ ≤ 0 := by linarith
_ ≤ ‖1 - Complex.exp (Complex.I * x)‖ := by apply norm_nonneg
Proof state after:
no goals
Theorem: lower_secant_bound
Proof state before:
η x : ℝ
xIcc : x ∈ Set.Icc (-2 * Real.pi + η) (2 * Real.pi - η)
xAbs : η ≤ |x|
ηpos : η < 0
⊢ η / 2 ≤ 0
Tactic:
linarith
Proof state after:
no goals
Theorem: lower_secant_bound
Proof state before:
η x : ℝ
xIcc : x ∈ Set.Icc (-2 * Real.pi + η) (2 * Real.pi - η)
xAbs : η ≤ |x|
ηpos : η < 0
⊢ 0 ≤ ‖1 - (Complex.I * ↑x).exp‖
Tactic:
apply norm_nonneg
Proof state after:
no goals
Theorem: lower_secant_bound
Proof state before:
η x : ℝ
xIcc : x ∈ Set.Icc (-2 * Real.pi + η) (2 * Real.pi - η)
xAbs : η ≤ |x|
ηpos : 0 ≤ η
⊢ η / 2 ≤ 2 / Real.pi * η
Tactic:
ring_nf
Proof state after:
η x : ℝ
xIcc : x ∈ Set.Icc (-2 * Real.pi + η) (2 * Real.pi - η)
xAbs : η ≤ |x|
ηpos : 0 ≤ η
⊢ η * (1 / 2) ≤ η * Real.pi⁻¹ * 2
Theorem: lower_secant_bound
Proof state before:
η x : ℝ
xIcc : x ∈ Set.Icc (-2 * Real.pi + η) (2 * Real.pi - η)
xAbs : η ≤ |x|
ηpos : 0 ≤ η
⊢ η * (1 / 2) ≤ η * Real.pi⁻¹ * 2
Tactic:
rw [mul_assoc]
Proof state after:
η x : ℝ
xIcc : x ∈ Set.Icc (-2 * Real.pi + η) (2 * Real.pi - η)
xAbs : η ≤ |x|
ηpos : 0 ≤ η
⊢ η * (1 / 2) ≤ η * (Real.pi⁻¹ * 2)
Theorem: lower_secant_bound
Proof state before:
η x : ℝ
xIcc : x ∈ Set.Icc (-2 * Real.pi + η) (2 * Real.pi - η)
xAbs : η ≤ |x|
ηpos : 0 ≤ η
⊢ η * (1 / 2) ≤ η * (Real.pi⁻¹ * 2)
Tactic:
gcongr
Proof state after:
case h
η x : ℝ
xIcc : x ∈ Set.Icc (-2 * Real.pi + η) (2 * Real.pi - η)
xAbs : η ≤ |x|
ηpos : 0 ≤ η
⊢ 1 / 2 ≤ Real.pi⁻¹ * 2
Theorem: lower_secant_bound
Proof state before:
case h
η x : ℝ
xIcc : x ∈ Set.Icc (-2 * Real.pi + η) (2 * Real.pi - η)
xAbs : η ≤ |x|
ηpos : 0 ≤ η
⊢ 1 / 2 ≤ Real.pi⁻¹ * 2
Tactic:
field_simp
Proof state after:
case h
η x : ℝ
xIcc : x ∈ Set.Icc (-2 * Real.pi + η) (2 * Real.pi - η)
xAbs : η ≤ |x|
ηpos : 0 ≤ η
⊢ 1 / 2 ≤ 2 / Real.pi
Theorem: lower_secant_bound
Proof state before:
case h
η x : ℝ
xIcc : x ∈ Set.Icc (-2 * Real.pi + η) (2 * Real.pi - η)
xAbs : η ≤ |x|
ηpos : 0 ≤ η
⊢ 1 / 2 ≤ 2 / Real.pi
Tactic:
rw [div_le_div_iff (by norm_num) Real.pi_pos]
Proof state after:
case h
η x : ℝ
xIcc : x ∈ Set.Icc (-2 * Real.pi + η) (2 * Real.pi - η)
xAbs : η ≤ |x|
ηpos : 0 ≤ η
⊢ 1 * Real.pi ≤ 2 * 2
Theorem: lower_secant_bound
Proof state before:
case h
η x : ℝ
xIcc : x ∈ Set.Icc (-2 * Real.pi + η) (2 * Real.pi - η)
xAbs : η ≤ |x|
ηpos : 0 ≤ η
⊢ 1 * Real.pi ≤ 2 * 2
Tactic:
linarith [Real.pi_le_four]
Proof state after:
no goals
Theorem: lower_secant_bound
Proof state before:
η x : ℝ
xIcc : x ∈ Set.Icc (-2 * Real.pi + η) (2 * Real.pi - η)
xAbs : η ≤ |x|
ηpos : 0 ≤ η
⊢ 0 < 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: lower_secant_bound
Proof state before:
η x : ℝ
xIcc : x ∈ Set.Icc (-2 * Real.pi + η) (2 * Real.pi - η)
xAbs : η ≤ |x|
ηpos : 0 ≤ η
⊢ 2 / Real.pi * η ≤ ‖1 - (Complex.I * ↑x).exp‖
Tactic:
apply lower_secant_bound' xAbs
Proof state after:
η x : ℝ
xIcc : x ∈ Set.Icc (-2 * Real.pi + η) (2 * Real.pi - η)
xAbs : η ≤ |x|
ηpos : 0 ≤ η
⊢ |x| ≤ 2 * Real.pi - η
Theorem: lower_secant_bound
Proof state before:
η x : ℝ
xIcc : x ∈ Set.Icc (-2 * Real.pi + η) (2 * Real.pi - η)
xAbs : η ≤ |x|
ηpos : 0 ≤ η
⊢ |x| ≤ 2 * Real.pi - η
Tactic:
rw [abs_le, neg_sub', sub_neg_eq_add, neg_mul_eq_neg_mul]
Proof state after:
η x : ℝ
xIcc : x ∈ Set.Icc (-2 * Real.pi + η) (2 * Real.pi - η)
xAbs : η ≤ |x|
ηpos : 0 ≤ η
⊢ -2 * Real.pi + η ≤ x ∧ x ≤ 2 * Real.pi - η
Theorem: lower_secant_bound
Proof state before:
η x : ℝ
xIcc : x ∈ Set.Icc (-2 * Real.pi + η) (2 * Real.pi - η)
xAbs : η ≤ |x|
ηpos : 0 ≤ η
⊢ -2 * Real.pi + η ≤ x ∧ x ≤ 2 * Real.pi - η
Tactic:
exact xIcc
Proof state after:
no goals
Theorem: volume_ball_four_le_same
Proof state before:
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x : X
r : ℝ
⊢ volume.real (ball x (4 * r)) ≤ A ^ 2 * volume.real (ball x r)
Tactic:
calc volume.real (ball x (4 * r))
    = volume.real (ball x (2 * (2 * r))) := by ring_nf
  _ ≤ A * volume.real (ball x (2 * r)) := by apply volume_ball_two_le_same
  _ ≤ A * (A * volume.real (ball x r)) := by gcongr; apply volume_ball_two_le_same
  _ = A ^ 2 * volume.real (ball x r) := by ring_nf
Proof state after:
no goals
Theorem: volume_ball_four_le_same
Proof state before:
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x : X
r : ℝ
⊢ volume.real (ball x (4 * r)) = volume.real (ball x (2 * (2 * r)))
Tactic:
ring_nf
Proof state after:
no goals
Theorem: volume_ball_four_le_same
Proof state before:
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x : X
r : ℝ
⊢ volume.real (ball x (2 * (2 * r))) ≤ A * volume.real (ball x (2 * r))
Tactic:
apply volume_ball_two_le_same
Proof state after:
no goals
Theorem: volume_ball_four_le_same
Proof state before:
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x : X
r : ℝ
⊢ A * volume.real (ball x (2 * r)) ≤ A * (A * volume.real (ball x r))
Tactic:
gcongr
Proof state after:
case h
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x : X
r : ℝ
⊢ volume.real (ball x (2 * r)) ≤ A * volume.real (ball x r)
Theorem: volume_ball_four_le_same
Proof state before:
case h
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x : X
r : ℝ
⊢ volume.real (ball x (2 * r)) ≤ A * volume.real (ball x r)
Tactic:
apply volume_ball_two_le_same
Proof state after:
no goals
Theorem: volume_ball_four_le_same
Proof state before:
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x : X
r : ℝ
⊢ A * (A * volume.real (ball x r)) = A ^ 2 * volume.real (ball x r)
Tactic:
ring_nf
Proof state after:
no goals
Theorem: volume_ball_le_same
Proof state before:
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x : X
r s r' : ℝ
hsp : s > 0
hs : r' ≤ s * r
⊢ volume.real (ball x r') ≤ As A s * volume.real (ball x r)
Tactic:
have hn (n : ℕ) : volume.real (ball x (2^n * r)) ≤ A^n * volume.real (ball x r) := by
  induction n
  case zero =>
    simp
  case succ m hm =>
    calc volume.real (ball x (2 ^ (Nat.succ m) * r))
        = volume.real (ball x (2 ^ (m+1) * r)) := by rfl
      _ = volume.real (ball x ((2 ^ m*2^1) * r)) := by norm_cast
      _ = volume.real (ball x (2 * 2 ^ m * r)) := by ring_nf
      _ ≤ A * volume.real (ball x (2 ^ m * r)) := by rw[mul_assoc]; norm_cast; apply volume_ball_two_le_same
      _ ≤ A * (↑(A ^ m) * volume.real (ball x r)) := by gcongr
      _ = A^(Nat.succ m) * volume.real (ball x r) := by rw[<- mul_assoc, pow_succ']
Proof state after:
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x : X
r s r' : ℝ
hsp : s > 0
hs : r' ≤ s * r
hn : ∀ (n : ℕ), volume.real (ball x (2 ^ n * r)) ≤ A ^ n * volume.real (ball x r)
⊢ volume.real (ball x r') ≤ As A s * volume.real (ball x r)
Theorem: volume_ball_le_same
Proof state before:
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x : X
r s r' : ℝ
hsp : s > 0
hs : r' ≤ s * r
hn : ∀ (n : ℕ), volume.real (ball x (2 ^ n * r)) ≤ A ^ n * volume.real (ball x r)
⊢ volume.real (ball x r') ≤ As A s * volume.real (ball x r)
Tactic:
have haux : s * r ≤ 2 ^ ⌈Real.log s / Real.log 2⌉₊ * r := by
  sorry
Proof state after:
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x : X
r s r' : ℝ
hsp : s > 0
hs : r' ≤ s * r
hn : ∀ (n : ℕ), volume.real (ball x (2 ^ n * r)) ≤ A ^ n * volume.real (ball x r)
haux : s * r ≤ 2 ^ ⌈s.log / Real.log 2⌉₊ * r
⊢ volume.real (ball x r') ≤ As A s * volume.real (ball x r)
Theorem: volume_ball_le_same
Proof state before:
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x : X
r s r' : ℝ
hsp : s > 0
hs : r' ≤ s * r
hn : ∀ (n : ℕ), volume.real (ball x (2 ^ n * r)) ≤ A ^ n * volume.real (ball x r)
haux : s * r ≤ 2 ^ ⌈s.log / Real.log 2⌉₊ * r
⊢ volume.real (ball x r') ≤ As A s * volume.real (ball x r)
Tactic:
have h1 : ball x r' ⊆ ball x (2 ^ ⌈Real.log s / Real.log 2⌉₊ * r) := by
  calc ball x r' ⊆ ball x (s * r) := by apply ball_subset_ball hs
      _ ⊆ ball x (2 ^ ⌈Real.log s / Real.log 2⌉₊ * r) := by apply ball_subset_ball haux
Proof state after:
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x : X
r s r' : ℝ
hsp : s > 0
hs : r' ≤ s * r
hn : ∀ (n : ℕ), volume.real (ball x (2 ^ n * r)) ≤ A ^ n * volume.real (ball x r)
haux : s * r ≤ 2 ^ ⌈s.log / Real.log 2⌉₊ * r
h1 : ball x r' ⊆ ball x (2 ^ ⌈s.log / Real.log 2⌉₊ * r)
⊢ volume.real (ball x r') ≤ As A s * volume.real (ball x r)
Theorem: volume_ball_le_same
Proof state before:
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x : X
r s r' : ℝ
hsp : s > 0
hs : r' ≤ s * r
hn : ∀ (n : ℕ), volume.real (ball x (2 ^ n * r)) ≤ A ^ n * volume.real (ball x r)
haux : s * r ≤ 2 ^ ⌈s.log / Real.log 2⌉₊ * r
h1 : ball x r' ⊆ ball x (2 ^ ⌈s.log / Real.log 2⌉₊ * r)
⊢ volume.real (ball x r') ≤ As A s * volume.real (ball x r)
Tactic:
calc volume.real (ball x r')
        ≤ volume.real (ball x (2 ^ ⌈Real.log s / Real.log 2⌉₊ * r)) := by gcongr; finiteness
      _ ≤ A^(⌈Real.log s / Real.log 2⌉₊) * volume.real (ball x r) := by apply hn
Proof state after:
no goals
Theorem: volume_ball_le_same
Proof state before:
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x : X
r s r' : ℝ
hsp : s > 0
hs : r' ≤ s * r
n : ℕ
⊢ volume.real (ball x (2 ^ n * r)) ≤ A ^ n * volume.real (ball x r)
Tactic:
induction n
Proof state after:
case zero
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x : X
r s r' : ℝ
hsp : s > 0
hs : r' ≤ s * r
⊢ volume.real (ball x (2 ^ 0 * r)) ≤ A ^ 0 * volume.real (ball x r)

case succ
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x : X
r s r' : ℝ
hsp : s > 0
hs : r' ≤ s * r
n✝ : ℕ
a✝ : volume.real (ball x (2 ^ n✝ * r)) ≤ A ^ n✝ * volume.real (ball x r)
⊢ volume.real (ball x (2 ^ (n✝ + 1) * r)) ≤ A ^ (n✝ + 1) * volume.real (ball x r)
Theorem: volume_ball_le_same
Proof state before:
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x : X
r s r' : ℝ
hsp : s > 0
hs : r' ≤ s * r
⊢ volume.real (ball x (2 ^ 0 * r)) ≤ A ^ 0 * volume.real (ball x r)
Tactic:
case zero =>
  simp
Proof state after:
no goals
Theorem: volume_ball_le_same
Proof state before:
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x : X
r s r' : ℝ
hsp : s > 0
hs : r' ≤ s * r
m : ℕ
hm : volume.real (ball x (2 ^ m * r)) ≤ A ^ m * volume.real (ball x r)
⊢ volume.real (ball x (2 ^ (m + 1) * r)) ≤ A ^ (m + 1) * volume.real (ball x r)
Tactic:
case succ m hm =>
  calc volume.real (ball x (2 ^ (Nat.succ m) * r))
      = volume.real (ball x (2 ^ (m+1) * r)) := by rfl
    _ = volume.real (ball x ((2 ^ m*2^1) * r)) := by norm_cast
    _ = volume.real (ball x (2 * 2 ^ m * r)) := by ring_nf
    _ ≤ A * volume.real (ball x (2 ^ m * r)) := by rw[mul_assoc]; norm_cast; apply volume_ball_two_le_same
    _ ≤ A * (↑(A ^ m) * volume.real (ball x r)) := by gcongr
    _ = A^(Nat.succ m) * volume.real (ball x r) := by rw[<- mul_assoc, pow_succ']
Proof state after:
no goals
Theorem: volume_ball_le_same
Proof state before:
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x : X
r s r' : ℝ
hsp : s > 0
hs : r' ≤ s * r
⊢ volume.real (ball x (2 ^ 0 * r)) ≤ A ^ 0 * volume.real (ball x r)
Tactic:
simp
Proof state after:
no goals
Theorem: volume_ball_le_same
Proof state before:
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x : X
r s r' : ℝ
hsp : s > 0
hs : r' ≤ s * r
m : ℕ
hm : volume.real (ball x (2 ^ m * r)) ≤ A ^ m * volume.real (ball x r)
⊢ volume.real (ball x (2 ^ (m + 1) * r)) ≤ A ^ (m + 1) * volume.real (ball x r)
Tactic:
calc volume.real (ball x (2 ^ (Nat.succ m) * r))
    = volume.real (ball x (2 ^ (m+1) * r)) := by rfl
  _ = volume.real (ball x ((2 ^ m*2^1) * r)) := by norm_cast
  _ = volume.real (ball x (2 * 2 ^ m * r)) := by ring_nf
  _ ≤ A * volume.real (ball x (2 ^ m * r)) := by rw[mul_assoc]; norm_cast; apply volume_ball_two_le_same
  _ ≤ A * (↑(A ^ m) * volume.real (ball x r)) := by gcongr
  _ = A^(Nat.succ m) * volume.real (ball x r) := by rw[<- mul_assoc, pow_succ']
Proof state after:
no goals
Theorem: volume_ball_le_same
Proof state before:
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x : X
r s r' : ℝ
hsp : s > 0
hs : r' ≤ s * r
m : ℕ
hm : volume.real (ball x (2 ^ m * r)) ≤ A ^ m * volume.real (ball x r)
⊢ volume.real (ball x (2 ^ m.succ * r)) = volume.real (ball x (2 ^ (m + 1) * r))
Tactic:
rfl
Proof state after:
no goals
Theorem: volume_ball_le_same
Proof state before:
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x : X
r s r' : ℝ
hsp : s > 0
hs : r' ≤ s * r
m : ℕ
hm : volume.real (ball x (2 ^ m * r)) ≤ A ^ m * volume.real (ball x r)
⊢ volume.real (ball x (2 ^ (m + 1) * r)) = volume.real (ball x (2 ^ m * 2 ^ 1 * r))
Tactic:
norm_cast
Proof state after:
no goals
Theorem: volume_ball_le_same
Proof state before:
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x : X
r s r' : ℝ
hsp : s > 0
hs : r' ≤ s * r
m : ℕ
hm : volume.real (ball x (2 ^ m * r)) ≤ A ^ m * volume.real (ball x r)
⊢ volume.real (ball x (2 ^ m * 2 ^ 1 * r)) = volume.real (ball x (2 * 2 ^ m * r))
Tactic:
ring_nf
Proof state after:
no goals
Theorem: volume_ball_le_same
Proof state before:
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x : X
r s r' : ℝ
hsp : s > 0
hs : r' ≤ s * r
m : ℕ
hm : volume.real (ball x (2 ^ m * r)) ≤ A ^ m * volume.real (ball x r)
⊢ volume.real (ball x (2 * 2 ^ m * r)) ≤ A * volume.real (ball x (2 ^ m * r))
Tactic:
rw[mul_assoc]
Proof state after:
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x : X
r s r' : ℝ
hsp : s > 0
hs : r' ≤ s * r
m : ℕ
hm : volume.real (ball x (2 ^ m * r)) ≤ A ^ m * volume.real (ball x r)
⊢ volume.real (ball x (2 * (2 ^ m * r))) ≤ A * volume.real (ball x (2 ^ m * r))
Theorem: volume_ball_le_same
Proof state before:
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x : X
r s r' : ℝ
hsp : s > 0
hs : r' ≤ s * r
m : ℕ
hm : volume.real (ball x (2 ^ m * r)) ≤ A ^ m * volume.real (ball x r)
⊢ volume.real (ball x (2 * (2 ^ m * r))) ≤ A * volume.real (ball x (2 ^ m * r))
Tactic:
norm_cast
Proof state after:
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x : X
r s r' : ℝ
hsp : s > 0
hs : r' ≤ s * r
m : ℕ
hm : volume.real (ball x (2 ^ m * r)) ≤ A ^ m * volume.real (ball x r)
⊢ volume.real (ball x (2 * (↑(2 ^ m) * r))) ≤ A * volume.real (ball x (↑(2 ^ m) * r))
Theorem: volume_ball_le_same
Proof state before:
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x : X
r s r' : ℝ
hsp : s > 0
hs : r' ≤ s * r
m : ℕ
hm : volume.real (ball x (2 ^ m * r)) ≤ A ^ m * volume.real (ball x r)
⊢ volume.real (ball x (2 * (↑(2 ^ m) * r))) ≤ A * volume.real (ball x (↑(2 ^ m) * r))
Tactic:
apply volume_ball_two_le_same
Proof state after:
no goals
Theorem: volume_ball_le_same
Proof state before:
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x : X
r s r' : ℝ
hsp : s > 0
hs : r' ≤ s * r
m : ℕ
hm : volume.real (ball x (2 ^ m * r)) ≤ A ^ m * volume.real (ball x r)
⊢ A * volume.real (ball x (2 ^ m * r)) ≤ A * (A ^ m * volume.real (ball x r))
Tactic:
gcongr
Proof state after:
no goals
Theorem: volume_ball_le_same
Proof state before:
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x : X
r s r' : ℝ
hsp : s > 0
hs : r' ≤ s * r
m : ℕ
hm : volume.real (ball x (2 ^ m * r)) ≤ A ^ m * volume.real (ball x r)
⊢ A * (A ^ m * volume.real (ball x r)) = A ^ m.succ * volume.real (ball x r)
Tactic:
rw[<- mul_assoc, pow_succ']
Proof state after:
no goals
Theorem: volume_ball_le_same
Proof state before:
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x : X
r s r' : ℝ
hsp : s > 0
hs : r' ≤ s * r
hn : ∀ (n : ℕ), volume.real (ball x (2 ^ n * r)) ≤ A ^ n * volume.real (ball x r)
⊢ s * r ≤ 2 ^ ⌈s.log / Real.log 2⌉₊ * r
Tactic:
sorry
Proof state after:
no goals
Theorem: volume_ball_le_same
Proof state before:
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x : X
r s r' : ℝ
hsp : s > 0
hs : r' ≤ s * r
hn : ∀ (n : ℕ), volume.real (ball x (2 ^ n * r)) ≤ A ^ n * volume.real (ball x r)
haux : s * r ≤ 2 ^ ⌈s.log / Real.log 2⌉₊ * r
⊢ ball x r' ⊆ ball x (2 ^ ⌈s.log / Real.log 2⌉₊ * r)
Tactic:
calc ball x r' ⊆ ball x (s * r) := by apply ball_subset_ball hs
    _ ⊆ ball x (2 ^ ⌈Real.log s / Real.log 2⌉₊ * r) := by apply ball_subset_ball haux
Proof state after:
no goals