DAO: La semana en Calculemus (4 de noviembre de 2022)

   0 ≤ dist x y

import topology.metric_space.basic
 
variables {X : Type*} [metric_space X]
variables x y : X
 
example : 0 ≤ dist x y :=
sorry

import topology.metric_space.basic
 
variables {X : Type*} [metric_space X]
variables x y : X
 
-- 1ª demostración
example : 0 ≤ dist x y :=
  have h1 : 2 * dist x y ≥ 0, by calc
    2 * dist x y = dist x y + dist x y : two_mul (dist x y)
             ... = dist x y + dist y x : by rw [dist_comm x y]
             ... ≥ dist x x            : dist_triangle x y x
             ... = 0                   : dist_self x,
  show 0 ≤ dist x y,
    by exact nonneg_of_mul_nonneg_left h1 zero_lt_two
 
-- 2ª demostración
example : 0 ≤ dist x y :=
-- by library_search
dist_nonneg

import data.real.basic tactic
 
example :
  ∀ {x y ε : ℝ}, 0 < ε → ε ≤ 1 → |x| < ε → |y| < ε → |x * y| < ε :=
sorry

import data.real.basic tactic
 
-- 1ª demostración
-- ===============
 
example :
  ∀ {x y ε : ℝ}, 0 < ε → ε ≤ 1 → |x| < ε → |y| < ε → |x * y| < ε :=
begin
  intros x y ε he1 he2 hx hy,
  by_cases h : (|x| = 0),
  { calc |x * y|
         = |x| * |y| : abs_mul x y
     ... = 0 * |y|   : by rw h
     ... = 0         : zero_mul (abs y)
     ... < ε         : he1 },
  { have h1 : 0 < |x|,
    { have h2 : 0 ≤ |x| := abs_nonneg x,
      show 0 < |x|,
        exact lt_of_le_of_ne h2 (ne.symm h) },
    calc |x * y|
         = |x| * |y| : abs_mul x y
     ... < |x| * ε   : (mul_lt_mul_left h1).mpr hy
     ... < ε * ε     : (mul_lt_mul_right he1).mpr hx
     ... ≤ 1 * ε     : (mul_le_mul_right he1).mpr he2
     ... = ε         : one_mul ε },
end
 
-- 2ª demostración
-- ===============
 
example :
  ∀ {x y ε : ℝ}, 0 < ε → ε ≤ 1 → |x| < ε → |y| < ε → |x * y| < ε :=
begin
  intros x y ε he1 he2 hx hy,
  by_cases h : (|x| = 0),
  { calc |x * y|
         = |x| * |y| : by apply abs_mul
     ... = 0 * |y|   : by rw h
     ... = 0         : by apply zero_mul
     ... < ε         : by apply he1 },
  { have h1 : 0 < |x|,
      { have h2 : 0 ≤ |x|,
          apply abs_nonneg,
        exact lt_of_le_of_ne h2 (ne.symm h) },
    calc |x * y|
         = |x| * |y| : by rw abs_mul
     ... < |x| * ε   : by apply (mul_lt_mul_left h1).mpr hy
     ... < ε * ε     : by apply (mul_lt_mul_right he1).mpr hx
     ... ≤ 1 * ε     : by apply (mul_le_mul_right he1).mpr he2
     ... = ε         : by rw [one_mul] },
end
 
-- 3ª demostración
-- ===============
 
example :
  ∀ {x y ε : ℝ}, 0 < ε → ε ≤ 1 → |x| < ε → |y| < ε → |x * y| < ε :=
begin
  intros x y ε he1 he2 hx hy,
  by_cases (|x| = 0),
  { by finish },
  { have : 0 < |x|, by finish,
    calc |x * y|
         = |x| * |y| : by rw abs_mul
     ... < |x| * ε   : by finish
     ... ≤ 1 * ε     : by nlinarith
     ... = ε         : by finish },
end

import data.real.basic
 
-- (cota_superior f a) se verifica si a es una cota superior de f.
def cota_superior (f : ℝ → ℝ) (a : ℝ) : Prop :=
∀ x, f x ≤ a
 
variables (f g : ℝ → ℝ)
variables (a b : ℝ)
 
example
  (hfa : cota_superior f a)
  (hgb : cota_superior g b)
  : cota_superior (λ x, f x + g x) (a + b) :=
sorry

import data.real.basic
 
-- (cota_superior f a) se verifica si a es una cota superior de f.
def cota_superior (f : ℝ → ℝ) (a : ℝ) : Prop :=
∀ x, f x ≤ a
 
variables (f g : ℝ → ℝ)
variables (a b : ℝ)
 
-- 1ª demostración
-- ===============
 
example
  (hfa : cota_superior f a)
  (hgb : cota_superior g b)
  : cota_superior (λ x, f x + g x) (a + b) :=
begin
  have h1 : ∀ x, f x + g x ≤ a + b,
  { intro x,
    have h1a : f x ≤ a := hfa x,
    have h1b : g x ≤ b := hgb x,
    show f x + g x ≤ a + b,
      by exact add_le_add (hfa x) (hgb x), },
  show cota_superior (λ x, f x + g x) (a + b),
    by exact h1,
end
 
-- 2ª demostración
-- ===============
 
example
  (hfa : cota_superior f a)
  (hgb : cota_superior g b)
  : cota_superior (λ x, f x + g x) (a + b) :=
begin
  intro x,
  dsimp,
  change f x + g x ≤ a + b,
  apply add_le_add,
  apply hfa,
  apply hgb
end
 
-- 3ª demostración
-- ===============
 
example
  (hfa : cota_superior f a)
  (hgb : cota_superior g b)
  : cota_superior (λ x, f x + g x) (a + b) :=
λ x, add_le_add (hfa x) (hgb x)

import data.real.basic
 
-- (cota_inferior f a) se verifica si a es una cota inferior de f.
def cota_inferior (f : ℝ → ℝ) (a : ℝ) : Prop :=
∀ x, a ≤ f x
 
variables (f g : ℝ → ℝ)
variables (a b : ℝ)
 
example
  (hfa : cota_inferior f a)
  (hgb : cota_inferior g b)
  : cota_inferior (λ x, f x + g x) (a + b) :=
sorry

import data.real.basic
 
-- (cota_inferior f a) se verifica si a es una cota inferior de f.
def cota_inferior (f : ℝ → ℝ) (a : ℝ) : Prop :=
∀ x, a ≤ f x
 
variables (f g : ℝ → ℝ)
variables (a b : ℝ)
 
-- 1ª demostración
-- ===============
 
example
  (hfa : cota_inferior f a)
  (hgb : cota_inferior g b)
  : cota_inferior (λ x, f x + g x) (a + b) :=
begin
  have h1 : ∀ x, a + b ≤ f x + g x,
  { intro x,
    have h1a : a ≤ f x := hfa x,
    have h1b : b ≤ g x := hgb x,
    show a + b ≤ f x + g x,
      by exact add_le_add (hfa x) (hgb x), },
  show cota_inferior (λ x, f x + g x) (a + b),
    by exact h1,
end
 
-- 2ª demostración
-- ===============
 
example
  (hfa : cota_inferior f a)
  (hgb : cota_inferior g b)
  : cota_inferior (λ x, f x + g x) (a + b) :=
begin
  intro x,
  dsimp,
  change a + b ≤ f x + g x,
  apply add_le_add,
  apply hfa,
  apply hgb
end
 
-- 3ª demostración
-- ===============
 
example
  (hfa : cota_inferior f a)
  (hgb : cota_inferior g b)
  : cota_inferior (λ x, f x + g x) (a + b) :=
λ x, add_le_add (hfa x) (hgb x)

import data.real.basic
variables (f g : ℝ → ℝ)
 
def no_negativa (f : ℝ → ℝ) : Prop := ∀ x, 0 ≤ f x
 
example
  (nnf : no_negativa f)
  (nng : no_negativa g)
  : no_negativa (f * g) :=
sorry

import data.real.basic
variables (f g : ℝ → ℝ)
 
def no_negativa (f : ℝ → ℝ) : Prop := ∀ x, 0 ≤ f x
 
-- 1ª demostración
-- ===============
 
example
  (nnf : no_negativa f)
  (nng : no_negativa g)
  : no_negativa (f * g) :=
begin
  have h1 : ∀x, 0 ≤ f x * g x,
  { intro x,
    have h2: 0 ≤ f x := nnf x,
    have h3: 0 ≤ g x := nng x,
    show 0 ≤ f x * g x,
      by exact mul_nonneg (nnf x) (nng x), },
  show no_negativa (f * g),
    by exact h1,
end
 
-- 2ª demostración
-- ===============
 
example
  (nnf : no_negativa f)
  (nng : no_negativa g)
  : no_negativa (f * g) :=
begin
  intro x,
  change 0 ≤ f x * g x,
  apply mul_nonneg,
  apply nnf,
  apply nng
end
 
-- 3ª demostración
-- ===============
 
example
  (nnf : no_negativa f)
  (nng : no_negativa g)
  : no_negativa (f * g) :=
λ x, mul_nonneg (nnf x) (nng x)