Documentation

Projects.RealAnalysis.RationalFn

inductive RealAnalysis.RationalFn (ι : Type u_1) :

Type u_1

one {ι : Type u_1} : RationalFn ι
var {ι : Type u_1} : ι → RationalFn ι
neg {ι : Type u_1} : RationalFn ι → RationalFn ι
inv {ι : Type u_1} : RationalFn ι → RationalFn ι
add {ι : Type u_1} : RationalFn ι → RationalFn ι → RationalFn ι
mul {ι : Type u_1} : RationalFn ι → RationalFn ι → RationalFn ι

Instances For

class RealAnalysis.RationalFn.Cnd (α : Type u_1) [ha₁ : AddGroup α] [ha₂ : DivInvMonoid α] :

h (x : α) : x * 0 = 0

Instances

instance RealAnalysis.RationalFn.instCndReal :

instance RealAnalysis.RationalFn.instCndForallNatReal :

Cnd (ℕ → ℝ)

@[instance_reducible]

instance RealAnalysis.RationalFn.instOne {ι : Type u_2} :

One (RationalFn ι)

Equations

RealAnalysis.RationalFn.instOne = { one := RealAnalysis.RationalFn.one }

theorem RealAnalysis.RationalFn.one_def {ι : Type u_2} :

@[instance_reducible]

instance RealAnalysis.RationalFn.instNeg {ι : Type u_2} :

Neg (RationalFn ι)

Equations

RealAnalysis.RationalFn.instNeg = { neg := RealAnalysis.RationalFn.neg }

theorem RealAnalysis.RationalFn.neg_def {ι : Type u_2} {a : RationalFn ι} :

-a = a.neg

@[instance_reducible]

instance RealAnalysis.RationalFn.instInv {ι : Type u_2} :

Inv (RationalFn ι)

Equations

RealAnalysis.RationalFn.instInv = { inv := RealAnalysis.RationalFn.inv }

theorem RealAnalysis.RationalFn.inv_def {ι : Type u_2} {a : RationalFn ι} :

@[instance_reducible]

instance RealAnalysis.RationalFn.instAdd {ι : Type u_2} :

Add (RationalFn ι)

Equations

RealAnalysis.RationalFn.instAdd = { add := RealAnalysis.RationalFn.add }

theorem RealAnalysis.RationalFn.add_def {ι : Type u_2} {a b : RationalFn ι} :

a + b = a.add b

@[instance_reducible]

instance RealAnalysis.RationalFn.instMul {ι : Type u_2} :

Mul (RationalFn ι)

Equations

RealAnalysis.RationalFn.instMul = { mul := RealAnalysis.RationalFn.mul }

theorem RealAnalysis.RationalFn.mul_def {ι : Type u_2} {a b : RationalFn ι} :

a * b = a.mul b

def RealAnalysis.RationalFn.sub {ι : Type u_2} (a b : RationalFn ι) :

Equations

a.sub b = a + -b

Instances For

def RealAnalysis.RationalFn.div {ι : Type u_2} (a b : RationalFn ι) :

Equations

a.div b = a * b⁻¹

Instances For

@[instance_reducible]

instance RealAnalysis.RationalFn.instSub {ι : Type u_2} :

Sub (RationalFn ι)

Equations

RealAnalysis.RationalFn.instSub = { sub := RealAnalysis.RationalFn.sub }

theorem RealAnalysis.RationalFn.sub_def {ι : Type u_2} {a b : RationalFn ι} :

a - b = a.sub b

@[instance_reducible]

instance RealAnalysis.RationalFn.instDiv {ι : Type u_2} :

Div (RationalFn ι)

Equations

RealAnalysis.RationalFn.instDiv = { div := RealAnalysis.RationalFn.div }

theorem RealAnalysis.RationalFn.div_def {ι : Type u_2} {a b : RationalFn ι} :

a / b = a.div b

def RealAnalysis.RationalFn.zero {ι : Type u_2} :

Equations

RealAnalysis.RationalFn.zero = 1 - 1

Instances For

@[instance_reducible]

instance RealAnalysis.RationalFn.instZero {ι : Type u_2} :

Zero (RationalFn ι)

Equations

RealAnalysis.RationalFn.instZero = { zero := RealAnalysis.RationalFn.zero }

theorem RealAnalysis.RationalFn.zero_def {ι : Type u_2} :

def RealAnalysis.RationalFn.pow {ι : Type u_2} (a : RationalFn ι) (n : ℕ) :

Equations

a.pow 0 = a * 0 + 1
a.pow n_2.succ = a.pow n_2 * a

Instances For

@[instance_reducible]

instance RealAnalysis.RationalFn.instPowNat {ι : Type u_2} :

Pow (RationalFn ι) ℕ

Equations

RealAnalysis.RationalFn.instPowNat = { pow := RealAnalysis.RationalFn.pow }

theorem RealAnalysis.RationalFn.pow_def {ι : Type u_2} {a : RationalFn ι} {n : ℕ} :

a ^ n = a.pow n

theorem RealAnalysis.RationalFn.pow_zero {ι : Type u_2} {a : RationalFn ι} :

a ^ 0 = a * 0 + 1

theorem RealAnalysis.RationalFn.pow_succ {ι : Type u_2} {a : RationalFn ι} {n : ℕ} :

a ^ (n + 1) = a ^ n * a

def RealAnalysis.RationalFn.ofNat {ι : Type u_2} (n : ℕ) :

Equations

RealAnalysis.RationalFn.ofNat 0 = 0
RealAnalysis.RationalFn.ofNat n_2.succ = RealAnalysis.RationalFn.ofNat n_2 + 1

Instances For

@[instance_reducible]

instance RealAnalysis.RationalFn.instOfNat {ι : Type u_2} {n : ℕ} :

OfNat (RationalFn ι) n

Equations

RealAnalysis.RationalFn.instOfNat = { ofNat := RealAnalysis.RationalFn.ofNat n }

theorem RealAnalysis.RationalFn.ofNat_def {ι : Type u_2} {n : ℕ} :

OfNat.ofNat n = ofNat n

def RealAnalysis.RationalFn.eval {α : Type u_1} [ha₁ : AddGroup α] [ha₂ : DivInvMonoid α] {ι : Type u_2} (a : RationalFn ι) (F : ι → α) :

α

Equations

RealAnalysis.RationalFn.one.eval F = 1
(RealAnalysis.RationalFn.var i).eval F = F i
a_2.neg.eval F = -a_2.eval F
a_2.inv.eval F = (a_2.eval F)⁻¹
(a_2.add b).eval F = a_2.eval F + b.eval F
(a_2.mul b).eval F = a_2.eval F * b.eval F

Instances For

def RealAnalysis.RationalFn.cnd {α : Type u_1} [ha₁ : AddGroup α] [ha₂ : DivInvMonoid α] {ι : Type u_2} (a : RationalFn ι) (F : ι → α) :

Equations

RealAnalysis.RationalFn.one.cnd F = True
(RealAnalysis.RationalFn.var i).cnd F = True
a_2.neg.cnd F = a_2.cnd F
a_2.inv.cnd F = (a_2.eval F ≠ 0 ∧ a_2.cnd F)
(a_2.add b).cnd F = (a_2.cnd F ∧ b.cnd F)
(a_2.mul b).cnd F = (a_2.cnd F ∧ b.cnd F)

Instances For

@[simp]

theorem RealAnalysis.RationalFn.eval_sub {α : Type u_1} [ha₁ : AddGroup α] [ha₂ : DivInvMonoid α] {ι : Type u_2} {a b : RationalFn ι} {F : ι → α} :

(a - b).eval F = a.eval F - b.eval F

@[simp]

theorem RealAnalysis.RationalFn.eval_div {α : Type u_1} [ha₁ : AddGroup α] [ha₂ : DivInvMonoid α] {ι : Type u_2} {a b : RationalFn ι} {F : ι → α} :

(a / b).eval F = a.eval F / b.eval F

@[simp]

theorem RealAnalysis.RationalFn.eval_zero {α : Type u_1} [ha₁ : AddGroup α] [ha₂ : DivInvMonoid α] {ι : Type u_2} {F : ι → α} :

eval 0 F = 0

@[simp]

theorem RealAnalysis.RationalFn.eval_ofNat_zero' {α : Type u_1} [ha₁ : AddGroup α] [ha₂ : DivInvMonoid α] {ι : Type u_2} {F : ι → α} :

(ofNat 0).eval F = 0

@[simp]

theorem RealAnalysis.RationalFn.eval_ofNat_succ' {α : Type u_1} [ha₁ : AddGroup α] [ha₂ : DivInvMonoid α] {ι : Type u_2} {F : ι → α} {n : ℕ} :

(ofNat (n + 1)).eval F = (ofNat n).eval F + 1

@[simp]

theorem RealAnalysis.RationalFn.eval_ofNat_zero {α : Type u_1} [ha₁ : AddGroup α] [ha₂ : DivInvMonoid α] {ι : Type u_2} {F : ι → α} :

(OfNat.ofNat 0).eval F = 0

@[simp]

theorem RealAnalysis.RationalFn.eval_ofNat_succ {α : Type u_1} [ha₁ : AddGroup α] [ha₂ : DivInvMonoid α] {ι : Type u_2} {F : ι → α} {n : ℕ} :

(OfNat.ofNat (n + 1)).eval F = (OfNat.ofNat n).eval F + 1

@[simp]

theorem RealAnalysis.RationalFn.eval_pow_zero {α : Type u_1} [ha₁ : AddGroup α] [ha₂ : DivInvMonoid α] [ha₃ : Cnd α] {ι : Type u_2} {a : RationalFn ι} {F : ι → α} :

(a ^ 0).eval F = 1

@[simp]

theorem RealAnalysis.RationalFn.eval_pow {α : Type u_1} [ha₁ : AddGroup α] [ha₂ : DivInvMonoid α] [ha₃ : Cnd α] {ι : Type u_2} {a : RationalFn ι} {F : ι → α} {n : ℕ} :

(a ^ n).eval F = a.eval F ^ n

@[simp]

theorem RealAnalysis.RationalFn.cnd_sub {α : Type u_1} [ha₁ : AddGroup α] [ha₂ : DivInvMonoid α] {ι : Type u_2} {a b : RationalFn ι} {F : ι → α} :

(a - b).cnd F ↔ a.cnd F ∧ b.cnd F

@[simp]

theorem RealAnalysis.RationalFn.cnd_div {α : Type u_1} [ha₁ : AddGroup α] [ha₂ : DivInvMonoid α] {ι : Type u_2} {a b : RationalFn ι} {F : ι → α} :

(a / b).cnd F ↔ a.cnd F ∧ b.eval F ≠ 0 ∧ b.cnd F

@[simp]

theorem RealAnalysis.RationalFn.cnd_zero' {α : Type u_1} [ha₁ : AddGroup α] [ha₂ : DivInvMonoid α] {ι : Type u_2} {F : ι → α} :

(ofNat 0).cnd F

@[simp]

theorem RealAnalysis.RationalFn.cnd_ofNat' {α : Type u_1} [ha₁ : AddGroup α] [ha₂ : DivInvMonoid α] {ι : Type u_2} {F : ι → α} {n : ℕ} :

(ofNat n).cnd F

@[simp]

theorem RealAnalysis.RationalFn.cnd_zero {α : Type u_1} [ha₁ : AddGroup α] [ha₂ : DivInvMonoid α] {ι : Type u_2} {F : ι → α} :

(OfNat.ofNat 0).cnd F

@[simp]

theorem RealAnalysis.RationalFn.cnd_ofNat {α : Type u_1} [ha₁ : AddGroup α] [ha₂ : DivInvMonoid α] {ι : Type u_2} {F : ι → α} {n : ℕ} :

(OfNat.ofNat n).cnd F

@[simp]

theorem RealAnalysis.RationalFn.cnd_pow {α : Type u_1} [ha₁ : AddGroup α] [ha₂ : DivInvMonoid α] {ι : Type u_2} {a : RationalFn ι} {F : ι → α} {n : ℕ} :

(a ^ n).cnd F ↔ a.cnd F

theorem RealAnalysis.tendsTo_of_rationalFn {ι : Type u_1} {A : ι → ℕ → ℝ} {L : ι → ℝ} {f : RationalFn ι} (h₁ : ∀ (i : ι), tendsTo (A i) (L i)) (h₂ : f.cnd L) :

tendsTo (f.eval A) (f.eval L)