Аналіз I, Додаток A.6

Деякі приклади доказів та квантифікаторів у Lean

declaration uses 'sorry'example : ¬ ∃ δ > 0, ∀ ε > (0:ℝ), 2 * δ < ε := by⊢ ¬∃ δ > 0, ∀ ε > 0, 2 * δ < ε sorryAll goals completed! 🐙open Real in /-- Твердження A.6.2. Наведений нижче доказ є дещо не ідіоматичним для Lean, але ілюструє, як реалізувати доказ типу "нехай ε буде величиною, яку буде обрано пізніше". -/ example : ∃ ε > 0, ∀ x, 0 < x ∧ x < ε → sin x > x / 2 := by⊢ ∃ ε > 0, ∀ (x : ℝ), 0 < x ∧ x < ε → sin x > x / 2 use ?epsh⊢ ?eps > 0 ∧ ∀ (x : ℝ), 0 < x ∧ x < ?eps → sin x > x / 2eps⊢ ℝ -- ми оберемо це пізніше constructorh.left⊢ ?eps > 0h.right⊢ ∀ (x : ℝ), 0 < x ∧ x < ?eps → sin x > x / 2eps⊢ ℝ swaph.right⊢ ∀ (x : ℝ), 0 < x ∧ x < ?eps → sin x > x / 2h.left⊢ ?eps > 0eps⊢ ℝ -- відкласти перевірку позитивності на потім intro x hxh.rightx:ℝhx:0 < x ∧ x < ?eps⊢ sin x > x / 2h.left⊢ ?eps > 0eps⊢ ℝ have hpos := hx.1h.rightx:ℝhx:0 < x ∧ x < ?epshpos:0 < x⊢ sin x > x / 2h.left⊢ ?eps > 0eps⊢ ℝ have hderiv : deriv sin = cos := by⊢ ∃ ε > 0, ∀ (x : ℝ), 0 < x ∧ x < ε → sin x > x / 2 ext xhx✝:ℝhx:0 < x✝ ∧ x✝ < ?epshpos:0 < x✝x:ℝ⊢ deriv sin x = cos x apply HasDerivAt.derivh.hx✝:ℝhx:0 < x✝ ∧ x✝ < ?epshpos:0 < x✝x:ℝ⊢ HasDerivAt sin (cos x) x apply hasDerivAt_sinAll goals completed! 🐙 have := exists_deriv_eq_slope sin hpos (byx:ℝhx:0 < x ∧ x < ?epshpos:0 < xhderiv:deriv sin = cos⊢ ContinuousOn sin (Set.Icc 0 x) fun_propAll goals completed! 🐙) (byx:ℝhx:0 < x ∧ x < ?epshpos:0 < xhderiv:deriv sin = cos⊢ DifferentiableOn ℝ sin (Set.Ioo 0 x) fun_propAll goals completed! 🐙) simp [hderiv] at thish.rightx:ℝhx:0 < x ∧ x < ?epshpos:0 < xhderiv:deriv sin = costhis:∃ c, (0 < c ∧ c < x) ∧ cos c = sin x / x⊢ sin x > x / 2h.left⊢ ?eps > 0eps⊢ ℝ obtain ⟨ y, ⟨ hy1, hy2 ⟩, hy3 ⟩ := thish.right.intro.intro.introx:ℝhx:0 < x ∧ x < ?epshpos:0 < xhderiv:deriv sin = cosy:ℝhy3:cos y = sin x / xhy1:0 < yhy2:y < x⊢ sin x > x / 2h.left⊢ ?eps > 0eps⊢ ℝ suffices hcosy : cos y > 1/2h.right.intro.intro.introx:ℝhx:0 < x ∧ x < ?epshpos:0 < xhderiv:deriv sin = cosy:ℝhy3:cos y = sin x / xhy1:0 < yhy2:y < xhcosy:cos y > 1 / 2⊢ sin x > x / 2hcosyx:ℝhx:0 < x ∧ x < ?epshpos:0 < xhderiv:deriv sin = cosy:ℝhy3:cos y = sin x / xhy1:0 < yhy2:y < x⊢ cos y > 1 / 2h.left⊢ ?eps > 0eps⊢ ℝ .h.right.intro.intro.introx:ℝhx:0 < x ∧ x < ?epshpos:0 < xhderiv:deriv sin = cosy:ℝhy3:cos y = sin x / xhy1:0 < yhy2:y < xhcosy:cos y > 1 / 2⊢ sin x > x / 2 rw [hy3, gt_iff_lt, ←(mul_lt_mul_left hpos)] at hcosyh.right.intro.intro.introx:ℝhx:0 < x ∧ x < ?epshpos:0 < xhderiv:deriv sin = cosy:ℝhy3:cos y = sin x / xhy1:0 < yhy2:y < xhcosy:x * (1 / 2) < x * (sin x / x)⊢ sin x > x / 2 rw [gt_iff_lt]h.right.intro.intro.introx:ℝhx:0 < x ∧ x < ?epshpos:0 < xhderiv:deriv sin = cosy:ℝhy3:cos y = sin x / xhy1:0 < yhy2:y < xhcosy:x * (1 / 2) < x * (sin x / x)⊢ x / 2 < sin x convert hcosy using 1h.e'_3x:ℝhx:0 < x ∧ x < ?epshpos:0 < xhderiv:deriv sin = cosy:ℝhy3:cos y = sin x / xhy1:0 < yhy2:y < xhcosy:x * (1 / 2) < x * (sin x / x)⊢ x / 2 = x * (1 / 2)h.e'_4x:ℝhx:0 < x ∧ x < ?epshpos:0 < xhderiv:deriv sin = cosy:ℝhy3:cos y = sin x / xhy1:0 < yhy2:y < xhcosy:x * (1 / 2) < x * (sin x / x)⊢ sin x = x * (sin x / x) .h.e'_3x:ℝhx:0 < x ∧ x < ?epshpos:0 < xhderiv:deriv sin = cosy:ℝhy3:cos y = sin x / xhy1:0 < yhy2:y < xhcosy:x * (1 / 2) < x * (sin x / x)⊢ x / 2 = x * (1 / 2) ringAll goals completed! 🐙 field_simpAll goals completed! 🐙 suffices ybound : y < π/3hcosyx:ℝhx:0 < x ∧ x < ?epshpos:0 < xhderiv:deriv sin = cosy:ℝhy3:cos y = sin x / xhy1:0 < yhy2:y < xybound:y < π / 3⊢ cos y > 1 / 2yboundx:ℝhx:0 < x ∧ x < ?epshpos:0 < xhderiv:deriv sin = cosy:ℝhy3:cos y = sin x / xhy1:0 < yhy2:y < x⊢ y < π / 3h.left⊢ ?eps > 0eps⊢ ℝ .hcosyx:ℝhx:0 < x ∧ x < ?epshpos:0 < xhderiv:deriv sin = cosy:ℝhy3:cos y = sin x / xhy1:0 < yhy2:y < xybound:y < π / 3⊢ cos y > 1 / 2 have := cos_lt_cos_of_nonneg_of_le_pi (le_of_lt hy1) (byx:ℝhx:0 < x ∧ x < ?epshpos:0 < xhderiv:deriv sin = cosy:ℝhy3:cos y = sin x / xhy1:0 < yhy2:y < xybound:y < π / 3⊢ π / 3 ≤ π linarithAll goals completed! 🐙) ybound simp only [cos_pi_div_three, ←gt_iff_lt] at thishcosyx:ℝhx:0 < x ∧ x < ?epshpos:0 < xhderiv:deriv sin = cosy:ℝhy3:cos y = sin x / xhy1:0 < yhy2:y < xybound:y < π / 3this:cos y > 1 / 2⊢ cos y > 1 / 2 exact thisAll goals completed! 🐙 have : y < ?eps := by⊢ ∃ ε > 0, ∀ (x : ℝ), 0 < x ∧ x < ε → sin x > x / 2 exact hy2.trans hx.2All goals completed! 🐙 pick_goal 3eps⊢ ℝyboundx:ℝhx:0 < x ∧ x < ?epshpos:0 < xhderiv:deriv sin = cosy:ℝhy3:cos y = sin x / xhy1:0 < yhy2:y < xthis:y < ?eps⊢ y < π / 3h.left⊢ ?eps > 0 -- Тепер час підібрати ε .eps⊢ ℝ exact π/3All goals completed! 🐙 exact thish.left⊢ π / 3 > 0 positivityAll goals completed! 🐙open Real in /-- Твердження A.6.2: більш ідіоматичний доказ -/ example : ∃ ε > 0, ∀ x, 0 < x ∧ x < ε → sin x > x / 2 := by⊢ ∃ ε > 0, ∀ (x : ℝ), 0 < x ∧ x < ε → sin x > x / 2 use π/3, by⊢ π / 3 > 0 positivityAll goals completed! 🐙 intro x ⟨ hpos, hx ⟩rightx:ℝhpos:0 < xhx:x < π / 3⊢ sin x > x / 2 have hderiv : deriv sin = cos := by⊢ ∃ ε > 0, ∀ (x : ℝ), 0 < x ∧ x < ε → sin x > x / 2 ext xhx✝:ℝhpos:0 < x✝hx:x✝ < π / 3x:ℝ⊢ deriv sin x = cos x apply HasDerivAt.derivh.hx✝:ℝhpos:0 < x✝hx:x✝ < π / 3x:ℝ⊢ HasDerivAt sin (cos x) x apply hasDerivAt_sinAll goals completed! 🐙 have := exists_deriv_eq_slope sin hpos (byx:ℝhpos:0 < xhx:x < π / 3hderiv:deriv sin = cos⊢ ContinuousOn sin (Set.Icc 0 x) fun_propAll goals completed! 🐙) (byx:ℝhpos:0 < xhx:x < π / 3hderiv:deriv sin = cos⊢ DifferentiableOn ℝ sin (Set.Ioo 0 x) fun_propAll goals completed! 🐙) simp [hderiv] at thisrightx:ℝhpos:0 < xhx:x < π / 3hderiv:deriv sin = costhis:∃ c, (0 < c ∧ c < x) ∧ cos c = sin x / x⊢ sin x > x / 2 obtain ⟨ y, ⟨ hy1, hy2 ⟩, hy3 ⟩ := thisright.intro.intro.introx:ℝhpos:0 < xhx:x < π / 3hderiv:deriv sin = cosy:ℝhy3:cos y = sin x / xhy1:0 < yhy2:y < x⊢ sin x > x / 2 have ybound : y < π/3 := by⊢ ∃ ε > 0, ∀ (x : ℝ), 0 < x ∧ x < ε → sin x > x / 2 linarithAll goals completed! 🐙 have hcosy := cos_lt_cos_of_nonneg_of_le_pi (le_of_lt hy1) (byx:ℝhpos:0 < xhx:x < π / 3hderiv:deriv sin = cosy:ℝhy3:cos y = sin x / xhy1:0 < yhy2:y < xybound:y < π / 3⊢ π / 3 ≤ π linarithAll goals completed! 🐙) ybound simp only [cos_pi_div_three, ←gt_iff_lt] at hcosyright.intro.intro.introx:ℝhpos:0 < xhx:x < π / 3hderiv:deriv sin = cosy:ℝhy3:cos y = sin x / xhy1:0 < yhy2:y < xybound:y < π / 3hcosy:cos y > 1 / 2⊢ sin x > x / 2 rw [hy3, gt_iff_lt, ←(mul_lt_mul_left hpos)] at hcosyright.intro.intro.introx:ℝhpos:0 < xhx:x < π / 3hderiv:deriv sin = cosy:ℝhy3:cos y = sin x / xhy1:0 < yhy2:y < xybound:y < π / 3hcosy:x * (1 / 2) < x * (sin x / x)⊢ sin x > x / 2 rw [gt_iff_lt]right.intro.intro.introx:ℝhpos:0 < xhx:x < π / 3hderiv:deriv sin = cosy:ℝhy3:cos y = sin x / xhy1:0 < yhy2:y < xybound:y < π / 3hcosy:x * (1 / 2) < x * (sin x / x)⊢ x / 2 < sin x convert hcosy using 1h.e'_3x:ℝhpos:0 < xhx:x < π / 3hderiv:deriv sin = cosy:ℝhy3:cos y = sin x / xhy1:0 < yhy2:y < xybound:y < π / 3hcosy:x * (1 / 2) < x * (sin x / x)⊢ x / 2 = x * (1 / 2)h.e'_4x:ℝhpos:0 < xhx:x < π / 3hderiv:deriv sin = cosy:ℝhy3:cos y = sin x / xhy1:0 < yhy2:y < xybound:y < π / 3hcosy:x * (1 / 2) < x * (sin x / x)⊢ sin x = x * (sin x / x) .h.e'_3x:ℝhpos:0 < xhx:x < π / 3hderiv:deriv sin = cosy:ℝhy3:cos y = sin x / xhy1:0 < yhy2:y < xybound:y < π / 3hcosy:x * (1 / 2) < x * (sin x / x)⊢ x / 2 = x * (1 / 2) ringAll goals completed! 🐙 field_simpAll goals completed! 🐙