6 octubre 2023 – Calculemus

El producto de funciones no negativas es no negativo

PorJosé A. Alonso 6 octubre 202310 octubre 2023

Demostrar con Lean4 que si \(f\) y \(g\) son funciones no negativas de \(ℝ\) en \(ℝ\), entonces su producto es no negativo.

Para ello, completar la siguiente teoría de Lean4:

import Mathlib.Data.Real.Basic

-- (CotaInferior f a) expresa que a es una cota inferior de f.
def CotaInferior (f : ℝ → ℝ) (a : ℝ) : Prop :=
  ∀ x, a ≤ f x

variable (f g : ℝ → ℝ)

example
  (nnf : CotaInferior f 0)
  (nng : CotaInferior g 0)
  : CotaInferior (f * g) 0 :=
by
sorry

import Mathlib.Data.Real.Basic

-- (CotaInferior f a) expresa que a es una cota inferior de f.

def CotaInferior (f : ℝ → ℝ) (a : ℝ) : Prop :=

∀ x, a ≤ f x

variable (f g : ℝ → ℝ)

example

(nnf : CotaInferior f 0)

(nng : CotaInferior g 0)

: CotaInferior (f * g) 0 :=

sorry