Prueba de (1+p)ⁿ ≥ 1+np
Sean p ∈ ℝ y n ∈ ℕ tales que p > -1. Demostrar que
1 |
(1 + p)ⁿ ≥ 1 + np |
Para ello, completar la siguiente teoría de Lean:
1 2 3 4 5 6 7 8 9 10 11 |
import data.real.basic open nat variable (p : ℝ) variable (n : ℕ) example (h : p > -1) : (1 + p)^n ≥ 1 + n*p := begin sorry |
[expand title=»Soluciones con Lean»]
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 |
import data.real.basic open nat variable (p : ℝ) variable (n : ℕ) set_option pp.structure_projections false example (h : p > -1) : (1 + p)^n ≥ 1 + n*p := begin induction n with n HI, { simp, }, { have h1 : 1 + p > 0 := iff.mp neg_lt_iff_pos_add' h, have h2 : p*p ≥ 0 := mul_self_nonneg p, replace h2 : ↑n*(p*p) ≥ 0 := mul_nonneg (cast_nonneg n) h2, calc (1 + p)^succ n = (1 + p)^n * (1 + p) : pow_succ' (1 + p) n ... ≥ (1 + n * p) * (1 + p) : (mul_le_mul_right h1).mpr HI ... = (1 + p + n*p) + n*(p*p) : by ring ! ... ≥ 1 + p + n*p : le_add_of_nonneg_right h2 ... = 1 + (n + 1) * p : by ring ! ... = 1 + ↑(succ n) * p : by norm_num }, end |
Se puede interactuar con la prueba anterior en esta sesión con Lean.
En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>
[/expand]
[expand title=»Soluciones con Isabelle/HOL»]
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 |
theory "Prueba_de_(1+p)^n_mayor_o_igual_que_1+np" imports Main HOL.Real begin lemma fixes p :: real assumes "p > -1" shows "(1 + p)^n ≥ 1 + n*p" proof (induct n) show "(1 + p) ^ 0 ≥ 1 + real 0 * p" by simp next fix n assume HI : "(1 + p)^n ≥ 1 + n * p" have "1 + Suc n * p = 1 + (n + 1) * p" by simp also have "… = 1 + n*p + p" by (simp add: distrib_right) also have "… ≤ (1 + n*p + p) + n*(p*p)" by simp also have "… = (1 + n * p) * (1 + p)" by algebra also have "… ≤ (1 + p)^n * (1 + p)" using HI assms by simp also have "… = (1 + p)^(Suc n)" by simp finally show "1 + Suc n * p ≤ (1 + p)^(Suc n)" . qed end |
En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]