mirror of
https://github.com/Smaug123/agdaproofs
synced 2025-10-07 21:08:39 +00:00
Base expansions do approximate the number (#114)
This commit is contained in:
Patrick Stevens
GitHub
@@ -8,7 +8,6 @@ open import Rings.Definition
|
||||
open import Sets.EquivalenceRelations
|
||||
open import Rings.IntegralDomains.Definition
|
||||
|
||||
|
||||
module Rings.IntegralDomains.Lemmas {m n : _} {A : Set n} {S : Setoid {n} {m} A} {_+_ _*_ : A → A → A} {R : Ring S _+_ _*_} (I : IntegralDomain R) where
|
||||
|
||||
open Setoid S
|
||||
@@ -24,3 +23,6 @@ cancelIntDom {a} {b} {c} ab=ac a!=0 = transferToRight (Ring.additiveGroup R) t3
|
||||
t2 = transitive (transitive (Ring.*DistributesOver+ R) (Group.+WellDefined (Ring.additiveGroup R) reflexive (transferToRight' (Ring.additiveGroup R) (transitive (symmetric (Ring.*DistributesOver+ R)) (transitive (Ring.*WellDefined R reflexive (Group.invLeft (Ring.additiveGroup R))) (Ring.timesZero R)))))) t1
|
||||
t3 : (b + Group.inverse (Ring.additiveGroup R) c) ∼ Ring.0R R
|
||||
t3 = IntegralDomain.intDom I t2 a!=0
|
||||
|
||||
cancelIntDom' : {a b c : A} → (a * c) ∼ (b * c) → (c ∼ Ring.0R R → False) → a ∼ b
|
||||
cancelIntDom' pr n = cancelIntDom (transitive *Commutative (transitive pr *Commutative)) n
|
||||
|
||||
@@ -18,6 +18,8 @@ open import Semirings.Definition
|
||||
open import Orders.Total.Definition
|
||||
open import Sequences
|
||||
|
||||
-- Note: totality is necessary here. The construction of a base-n expansion fundamentally relies on being able to take floors.
|
||||
|
||||
module Rings.Orders.Total.BaseExpansion {a m p : _} {A : Set a} {S : Setoid {a} {m} A} {_+_ : A → A → A} {_*_ : A → A → A} {R : Ring S _+_ _*_} {_<_ : Rel {_} {p} A} {pOrder : SetoidPartialOrder S _<_} {pOrderRing : PartiallyOrderedRing R pOrder} (order : TotallyOrderedRing pOrderRing) {n : ℕ} (1<n : 1 <N n) where
|
||||
|
||||
open Ring R
|
||||
@@ -32,6 +34,7 @@ open import Rings.Lemmas R
|
||||
open import Rings.Orders.Partial.Lemmas pOrderRing
|
||||
open import Rings.Orders.Total.Lemmas order
|
||||
open import Rings.InitialRing R
|
||||
open import Rings.IntegralDomains.Lemmas
|
||||
|
||||
record FloorIs (a : A) (n : ℕ) : Set (m ⊔ p) where
|
||||
field
|
||||
@@ -47,6 +50,9 @@ private
|
||||
0<n : {x y : A} → (x < y) → 0R < fromN n
|
||||
0<n x<y = fromNPreservesOrder (anyComparisonImpliesNontrivial x<y) (lessTransitive (succIsPositive 0) 1<n)
|
||||
|
||||
0<aFromN : {a : A} → (0<a : 0R < a) → 0R < (a * fromN n)
|
||||
0<aFromN 0<a = orderRespectsMultiplication 0<a (0<n 0<a)
|
||||
|
||||
floorWellDefinedLemma : {a : A} {n1 n2 : ℕ} → FloorIs a n1 → FloorIs a n2 → n1 <N n2 → False
|
||||
floorWellDefinedLemma {a} {n1} {n2} record { prAbove = prAbove1 } record { prBelow = inl prBelow } n1<n2 with TotalOrder.totality ℕTotalOrder (succ n1) n2
|
||||
... | inl (inl n1+1<n2) = irreflexive (<Transitive prAbove1 (<Transitive (fromNPreservesOrder (anyComparisonImpliesNontrivial prBelow) n1+1<n2) prBelow))
|
||||
@@ -69,8 +75,8 @@ private
|
||||
FloorIs.prBelow (floorWellDefined' {a} {b} {n} a=b record { prBelow = (inr x) ; prAbove = s }) = inr (transitive x a=b)
|
||||
FloorIs.prAbove (floorWellDefined' {a} {b} {n} a=b record { prBelow = t ; prAbove = s }) = <WellDefined a=b reflexive s
|
||||
|
||||
computeFloor' : {k : ℕ} → (fuel : ℕ) → k +N fuel ≡ n → (a : A) → 0R < a → a < fromN k → Sg ℕ (FloorIs a)
|
||||
computeFloor' {zero} zero refl a 0<a a<f = exFalso (lessIrreflexive (lessTransitive 1<n (succIsPositive 0)))
|
||||
computeFloor' : {k : ℕ} → (fuel : ℕ) → .(k +N fuel ≡ n) → (a : A) → (0R < a) → .(a < fromN k) → Sg ℕ (FloorIs a)
|
||||
computeFloor' {zero} zero pr a 0<a a<f = exFalso (lessIrreflexive (lessTransitive 1<n (le 0 (applyEquality succ (equalityCommutative pr)))))
|
||||
computeFloor' {zero} (succ k) pr a 0<a a<f = exFalso (irreflexive (<Transitive 0<a a<f))
|
||||
computeFloor' {succ k} n pr a 0<a a<f with totality 1R a
|
||||
... | inl (inr a<1) = 0 , (record { prAbove = <WellDefined reflexive (symmetric identRight) a<1 ; prBelow = inl 0<a })
|
||||
@@ -78,16 +84,123 @@ private
|
||||
... | inl (inl 1<a) with computeFloor' {k} (succ n) (transitivity (transitivity (Semiring.commutative ℕSemiring k (succ n)) (applyEquality succ (Semiring.commutative ℕSemiring n k))) pr) (a + inverse 1R) (moveInequality 1<a) (<WellDefined reflexive (transitive groupIsAbelian (transitive +Associative (transitive (+WellDefined invLeft reflexive) identLeft))) (orderRespectsAddition a<f (inverse 1R)))
|
||||
... | N , snd = succ N , floorWellDefined' (transitive (symmetric +Associative) (transitive (+WellDefined reflexive invLeft) identRight)) (addOneToFloor snd)
|
||||
|
||||
computeFloor : (a : A) → 0R < a → a < fromN n → Sg (ℤn n (lessTransitive (succIsPositive 0) 1<n)) (λ z → FloorIs a (ℤn.x z))
|
||||
computeFloor : (a : A) → (0R < a) → .(a < fromN n) → Sg (ℤn n (lessTransitive (succIsPositive 0) 1<n)) (λ z → FloorIs a (ℤn.x z))
|
||||
computeFloor a 0<a a<n with computeFloor' {n} 0 (Semiring.sumZeroRight ℕSemiring n) a 0<a a<n
|
||||
... | floor , record { prBelow = inl p ; prAbove = prAbove } = record { x = floor ; xLess = fromNPreservesOrder' (anyComparisonImpliesNontrivial 0<a) (<Transitive p a<n) } , record { prBelow = inl p ; prAbove = prAbove }
|
||||
... | floor , record { prBelow = inr p ; prAbove = prAbove } = record { x = floor ; xLess = fromNPreservesOrder' (anyComparisonImpliesNontrivial 0<a) (<WellDefined (symmetric p) reflexive a<n) } , record { prBelow = inr p ; prAbove = prAbove }
|
||||
|
||||
firstDigit : (a : A) → 0R < a → a < 1R → ℤn n (lessTransitive (succIsPositive 0) 1<n)
|
||||
firstDigit : (a : A) → 0R < a → .(a < 1R) → ℤn n (lessTransitive (succIsPositive 0) 1<n)
|
||||
firstDigit a 0<a a<1 = underlying (computeFloor (a * fromN n) (orderRespectsMultiplication 0<a (0<n 0<a)) (<WellDefined reflexive identIsIdent (ringCanMultiplyByPositive (0<n 0<a) a<1)))
|
||||
|
||||
baseNExpansion : (a : A) → 0R < a → a < 1R → Sequence (ℤn n (lessTransitive (succIsPositive 0) 1<n))
|
||||
baseNExpansion : (a : A) → 0R < a → .(a < 1R) → Sequence (ℤn n (lessTransitive (succIsPositive 0) 1<n))
|
||||
Sequence.head (baseNExpansion a 0<a a<1) = firstDigit a 0<a a<1
|
||||
Sequence.tail (baseNExpansion a 0<a a<1) with computeFloor (a * fromN n) (orderRespectsMultiplication 0<a (0<n 0<a)) (<WellDefined reflexive identIsIdent (ringCanMultiplyByPositive (0<n 0<a) a<1))
|
||||
Sequence.tail (baseNExpansion a 0<a a<1) with computeFloor (a * fromN n) (0<aFromN 0<a) (<WellDefined reflexive identIsIdent (ringCanMultiplyByPositive (0<n 0<a) a<1))
|
||||
... | record { x = x ; xLess = xLess } , record { prBelow = inl prB ; prAbove = prA } = baseNExpansion ((a * fromN n) + inverse (fromN x)) (moveInequality prB) (<WellDefined reflexive (transitive (symmetric +Associative) (transitive (+WellDefined reflexive invRight) identRight)) (orderRespectsAddition prA (inverse (fromN x))))
|
||||
... | record { x = x ; xLess = xLess } , record { prBelow = inr prB ; prAbove = prA } = constSequence (record { x = 0 ; xLess = lessTransitive (succIsPositive 0) 1<n })
|
||||
|
||||
private
|
||||
powerSeq : (i : A) → (start : A) → Sequence A
|
||||
Sequence.head (powerSeq i start) = start
|
||||
Sequence.tail (powerSeq i start) = powerSeq i (start * i)
|
||||
|
||||
powerSeqInduction : (i : A) (start : A) → (m : ℕ) → (index (powerSeq i start) (succ m)) ∼ i * (index (powerSeq i start) m)
|
||||
powerSeqInduction i start zero = *Commutative
|
||||
powerSeqInduction i start (succ m) = powerSeqInduction i (start * i) m
|
||||
|
||||
powerSeq' : (i : A) → Sequence A
|
||||
powerSeq' i = powerSeq i i
|
||||
|
||||
dot : A → ℤn n (lessTransitive (succIsPositive 0) 1<n) → A
|
||||
dot 1/n^i x = fromN (ℤn.x {n} {lessTransitive (succIsPositive 0) 1<n} x) * 1/n^i
|
||||
|
||||
dotWellDefined : {x y : A} {b : ℤn n (lessTransitive (succIsPositive 0) 1<n)} → (x ∼ y) → dot x b ∼ dot y b
|
||||
dotWellDefined eq = *WellDefined reflexive eq
|
||||
|
||||
sequenceEntries : (b : A) → (b * fromN n ∼ 1R) → Sequence (ℤn n (lessTransitive (succIsPositive 0) 1<n)) → Sequence A
|
||||
sequenceEntries 1/n pr1/n s = apply dot (powerSeq' 1/n) s
|
||||
|
||||
private
|
||||
partialSums' : A → Sequence A → Sequence A
|
||||
Sequence.head (partialSums' a seq) = a + Sequence.head seq
|
||||
Sequence.tail (partialSums' a seq) = partialSums' (a + Sequence.head seq) (Sequence.tail seq)
|
||||
|
||||
partialSums'WellDefined : (a b : A) → (a ∼ b) → (s : Sequence A) → (m : ℕ) → (index (partialSums' a s) m) ∼ (index (partialSums' b s) m)
|
||||
partialSums'WellDefined a b a=b s zero = +WellDefined a=b reflexive
|
||||
partialSums'WellDefined a b a=b s (succ m) = partialSums'WellDefined (a + Sequence.head s) (b + Sequence.head s) (+WellDefined a=b reflexive) (Sequence.tail s) m
|
||||
|
||||
partialSums'WellDefined' : (a : A) → (s1 s2 : Sequence A) → (equal : (m : ℕ) → index s1 m ∼ index s2 m) → (m : ℕ) → (index (partialSums' a s1) m) ∼ (index (partialSums' a s2) m)
|
||||
partialSums'WellDefined' a s1 s2 equal zero = +WellDefined reflexive (equal 0)
|
||||
partialSums'WellDefined' a s1 s2 equal (succ m) = transitive (partialSums'WellDefined (a + Sequence.head s1) (a + Sequence.head s2) (+WellDefined reflexive (equal 0)) _ m) (partialSums'WellDefined' (a + Sequence.head s2) (Sequence.tail s1) (Sequence.tail s2) (λ m → equal (succ m)) m)
|
||||
|
||||
partialSums'Translate : (a b : A) → (s : Sequence A) → (m : ℕ) → (index (partialSums' (a + b) s) m) ∼ (b + index (partialSums' a s) m)
|
||||
partialSums'Translate a b s zero = transitive (+WellDefined groupIsAbelian reflexive) (symmetric +Associative)
|
||||
partialSums'Translate a b s (succ m) = transitive (partialSums'WellDefined _ _ (transitive (symmetric +Associative) (transitive (+WellDefined reflexive groupIsAbelian) +Associative)) (Sequence.tail s) m) (partialSums'Translate (a + Sequence.head s) b (Sequence.tail s) m)
|
||||
|
||||
powerSeqWellDefined : {a b start1 start2 : A} → (a ∼ b) → (start1 ∼ start2) → (m : ℕ) → (index (powerSeq a start1) m) ∼ (index (powerSeq b start2) m)
|
||||
powerSeqWellDefined {a} {b} {s1} {s2} a=b s1=s2 zero = s1=s2
|
||||
powerSeqWellDefined {a} {b} {s1} {s2} a=b s1=s2 (succ m) = powerSeqWellDefined a=b (*WellDefined s1=s2 a=b) m
|
||||
|
||||
powerSeqMove : (a start : A) (m : ℕ) → index (powerSeq a (a * start)) m ∼ a * index (powerSeq a start) m
|
||||
powerSeqMove a start zero = reflexive
|
||||
powerSeqMove a start (succ m) = transitive (powerSeqWellDefined reflexive (transitive *Commutative (*WellDefined reflexive *Commutative)) m) (powerSeqMove _ _ m)
|
||||
|
||||
partialSumsConst : (r s : A) → (m : ℕ) → index (partialSums' r (constSequence s)) m ∼ (r + (s * fromN (succ m)))
|
||||
partialSumsConst r s zero = +WellDefined reflexive (transitive (symmetric identIsIdent) (transitive *Commutative (*WellDefined reflexive (symmetric identRight))))
|
||||
partialSumsConst r s (succ m) = transitive (partialSumsConst (r + s) s m) (transitive (symmetric +Associative) (+WellDefined reflexive (transitive (+WellDefined (symmetric (transitive *Commutative identIsIdent)) reflexive) (symmetric *DistributesOver+))))
|
||||
|
||||
applyWellDefined : {b : _} {B : Set b} (r1 r2 : Sequence A) (s : Sequence B) → (f : A → B → A) → ({x y : A} {b : B} → (x ∼ y) → f x b ∼ f y b) → ((m : ℕ) → index r1 m ∼ index r2 m) → (m : ℕ) → index (apply f r1 s) m ∼ index (apply f r2 s) m
|
||||
applyWellDefined r1 r2 s f wd eq zero = wd (eq 0)
|
||||
applyWellDefined r1 r2 s f wd eq (succ m) = applyWellDefined _ _ (Sequence.tail s) f wd (λ n → eq (succ n)) m
|
||||
|
||||
partialSums : Sequence A → Sequence A
|
||||
partialSums = partialSums' 0R
|
||||
|
||||
approximations : (b : A) → (b * (fromN n) ∼ 1R) → Sequence (ℤn n (lessTransitive (succIsPositive 0) 1<n)) → Sequence A
|
||||
approximations 1/n pr1/n s = partialSums (sequenceEntries 1/n pr1/n s)
|
||||
|
||||
private
|
||||
multiplyZeroSequence : (s : Sequence A) (m : ℕ) → index (apply dot s (constSequence (record { x = 0 ; xLess = lessTransitive (succIsPositive 0) 1<n }))) m ∼ 0R
|
||||
multiplyZeroSequence s zero = timesZero'
|
||||
multiplyZeroSequence s (succ m) = multiplyZeroSequence _ m
|
||||
|
||||
lemma1 : (x y : A) (s : Sequence (ℤn n (lessTransitive (succIsPositive 0) 1<n))) → (m : ℕ) → index (apply dot (powerSeq x (y * x)) s) m ∼ x * (index (apply dot (powerSeq x y) s) m)
|
||||
lemma1 x y s zero = transitive *Associative *Commutative
|
||||
lemma1 x y s (succ m) = lemma1 x (y * x) (Sequence.tail s) m
|
||||
|
||||
lemma2 : (w x y z : A) (s : Sequence (ℤn n (lessTransitive (succIsPositive 0) 1<n))) → (m : ℕ) → (w * index (partialSums' x (apply dot (powerSeq y z) s)) m) ∼ index (partialSums' (w * x) (apply dot (powerSeq y (z * w)) s)) m
|
||||
lemma2 x y z w s zero = transitive *DistributesOver+ (+WellDefined reflexive (transitive (transitive (*WellDefined reflexive *Commutative) (transitive *Associative (*WellDefined *Commutative reflexive))) *Commutative))
|
||||
lemma2 x y z w s (succ m) = transitive (lemma2 x (y + dot w (Sequence.head s)) z (w * z) (Sequence.tail s) m) (transitive (partialSums'WellDefined _ (_ + dot (w * x) (Sequence.head s)) (transitive *DistributesOver+ (+WellDefined reflexive (transitive *Commutative (symmetric *Associative)))) _ m) (partialSums'WellDefined' _ _ _ (λ n → applyWellDefined (powerSeq z ((w * z) * x)) (powerSeq z ((w * x) * z)) (Sequence.tail s) dot (λ {m} {n} {s} m=n → dotWellDefined {m} {n} {s} m=n) (λ n → powerSeqWellDefined reflexive (transitive (transitive (symmetric *Associative) (*WellDefined reflexive *Commutative)) *Associative) n) n) m))
|
||||
|
||||
approximationComesFromBelow : (1/n : A) → (1/nPr : 1/n * (fromN n) ∼ 1R) → (a : A) → (0<a : 0R < a) → (a<1 : a < 1R) → (m : ℕ) → index (approximations 1/n 1/nPr (baseNExpansion a 0<a a<1)) m <= a
|
||||
approximationComesFromBelow 1/n 1/nPr a 0<a a<1 zero with computeFloor' 0 (Semiring.sumZeroRight ℕSemiring n) (a * fromN n) (0<aFromN 0<a) ((<WellDefined reflexive identIsIdent (ringCanMultiplyByPositive (0<n 0<a) a<1)))
|
||||
... | x , record { prBelow = inl prBelow ; prAbove = prAbove } = inl (<WellDefined (symmetric identLeft) reflexive (ringCanCancelPositive (0<n prBelow) (<WellDefined (transitive (symmetric identIsIdent) (transitive *Commutative (transitive (*WellDefined reflexive (symmetric 1/nPr)) *Associative))) reflexive prBelow)))
|
||||
... | x , record { prBelow = inr prBelow ; prAbove = prAbove } = inr (transitive identLeft (transitive (transitive (transitive (transitive (*WellDefined prBelow reflexive) (transitive (symmetric *Associative) (*WellDefined reflexive *Commutative))) (*WellDefined reflexive 1/nPr)) (*Commutative)) identIsIdent))
|
||||
approximationComesFromBelow 1/n 1/nPr a 0<a a<1 (succ m) with computeFloor' 0 (Semiring.sumZeroRight ℕSemiring n) (a * fromN n) (0<aFromN 0<a) ((<WellDefined reflexive identIsIdent (ringCanMultiplyByPositive (0<n 0<a) a<1)))
|
||||
... | x , record { prBelow = inr x=an ; prAbove = an<x+1 } = inr (transitive (partialSums'Translate 0G _ _ m) (transitive (+WellDefined (transitive (*WellDefined x=an reflexive) (transitive (symmetric *Associative) (*WellDefined reflexive (transitive *Commutative 1/nPr)))) reflexive) (transitive (+WellDefined (transitive *Commutative identIsIdent) (transitive (partialSums'WellDefined' 0G _ (constSequence 0G) (λ m → transitive (multiplyZeroSequence (powerSeq 1/n (1/n * 1/n)) m) (identityOfIndiscernablesRight _∼_ reflexive (equalityCommutative (indexAndConst 0G m)))) m) (transitive (partialSumsConst _ _ m) (transitive identLeft timesZero')))) identRight)))
|
||||
... | x , record { prBelow = inl x<an ; prAbove = an<x+1 } with approximationComesFromBelow 1/n 1/nPr ((a * fromN n) + inverse (fromN x)) (moveInequality x<an) (<WellDefined reflexive (transitive (symmetric +Associative) (transitive (+WellDefined reflexive invRight) identRight)) (orderRespectsAddition an<x+1 (inverse (fromN x)))) m
|
||||
... | inl inter<an = inl (<WellDefined (symmetric (partialSums'Translate 0G (fromN x * 1/n) _ m)) reflexive (<WellDefined (+WellDefined reflexive (symmetric (partialSums'WellDefined 0G (fromN n * 0G) (symmetric timesZero) _ m))) reflexive (ringCanCancelPositive (0<n an<x+1) (<WellDefined (symmetric (transitive *DistributesOver+' (+WellDefined (transitive (symmetric *Associative) (transitive (*WellDefined reflexive 1/nPr) (transitive *Commutative identIsIdent))) (transitive *Commutative (transitive (lemma2 (fromN n) (fromN n * 0G) 1/n (1/n * 1/n) _ m) (transitive (partialSums'WellDefined _ 0G (transitive (*WellDefined reflexive timesZero) timesZero) _ m) (partialSums'WellDefined' 0G _ _ (λ m → applyWellDefined _ _ _ dot (λ {x} {y} {s} → dotWellDefined {x} {y} {s}) (λ m → powerSeqWellDefined {_} {1/n} {_} {1/n} reflexive (transitive (symmetric *Associative) (transitive (transitive *Commutative (*WellDefined 1/nPr reflexive)) identIsIdent)) m) m) m))))))) reflexive (<WellDefined groupIsAbelian (transitive (symmetric +Associative) (transitive (+WellDefined reflexive invLeft) identRight)) (orderRespectsAddition inter<an (fromN x)))))))
|
||||
... | inr inter=an = inr (transitive (partialSums'Translate 0G (fromN x * 1/n) _ m) (cancelIntDom' (isIntDom λ t → anyComparisonImpliesNontrivial a<1 (symmetric t)) ans λ t → irreflexive (<WellDefined reflexive t (fromNPreservesOrder (anyComparisonImpliesNontrivial a<1) (lessTransitive (succIsPositive 0) 1<n)))))
|
||||
where
|
||||
ans : (((fromN x * 1/n) + index (partialSums' 0G (apply dot (powerSeq 1/n (1/n * 1/n)) (baseNExpansion ((a * fromN n) + inverse (fromN x)) (moveInequality x<an) (<WellDefined reflexive (transitive (symmetric +Associative) (transitive (+WellDefined reflexive invRight) identRight)) (orderRespectsAddition an<x+1 (inverse (fromN x))))))) m) * fromN n) ∼ a * fromN n
|
||||
ans = transitive (transitive *DistributesOver+' (+WellDefined (transitive (symmetric *Associative) (transitive (*WellDefined reflexive 1/nPr) (transitive *Commutative identIsIdent))) *Commutative)) (transitive (+WellDefined reflexive (transitive (lemma2 (fromN n) 0G 1/n (1/n * 1/n) _ m) (transitive (partialSums'WellDefined _ _ timesZero _ m) (partialSums'WellDefined' _ _ _ (λ m → applyWellDefined _ _ _ dot (λ {x} {y} {s} → dotWellDefined {x} {y} {s}) (λ m → powerSeqWellDefined reflexive (transitive (symmetric *Associative) (transitive (*WellDefined reflexive 1/nPr) (transitive *Commutative identIsIdent))) m) m) m)))) (transitive (+WellDefined reflexive inter=an) (transitive groupIsAbelian (transitive (symmetric +Associative) (transitive (+WellDefined reflexive invLeft) identRight)))))
|
||||
|
||||
pow : ℕ → A → A
|
||||
pow zero x = 1R
|
||||
pow (succ n) x = x * pow n x
|
||||
|
||||
powPos : (m : ℕ) {a : A} → (0R < a) → 0R < pow m a
|
||||
powPos zero 0<a = 0<1 (anyComparisonImpliesNontrivial 0<a)
|
||||
powPos (succ m) 0<a = orderRespectsMultiplication 0<a (powPos m 0<a)
|
||||
|
||||
approximationIsNear : (1/n : A) → (1/nPr : 1/n * (fromN n) ∼ 1R) → (a : A) → (0<a : 0R < a) → (a<1 : a < 1R) → (m : ℕ) → a < ((index (approximations 1/n 1/nPr (baseNExpansion a 0<a a<1)) m) + pow m 1/n)
|
||||
approximationIsNear 1/n 1/npr a 0<a a<1 zero with computeFloor' 0 (Semiring.sumZeroRight ℕSemiring n) (a * fromN n) (0<aFromN 0<a) (<WellDefined reflexive identIsIdent (ringCanMultiplyByPositive (0<n 0<a) a<1))
|
||||
... | x , record { prBelow = inl prBelow ; prAbove = prAbove } = <WellDefined reflexive (transitive (symmetric identLeft) +Associative) (ringCanCancelPositive (0<n prAbove) (<Transitive prAbove (<WellDefined reflexive (transitive (+WellDefined (transitive (*WellDefined reflexive (symmetric 1/npr)) *Associative) (symmetric identIsIdent)) (symmetric *DistributesOver+')) (<WellDefined reflexive (transitive groupIsAbelian (+WellDefined (transitive (symmetric identIsIdent) *Commutative) reflexive)) (orderRespectsAddition (<WellDefined identRight reflexive (fromNPreservesOrder (anyComparisonImpliesNontrivial prAbove) 1<n)) (fromN x))))))
|
||||
... | x , record { prBelow = inr prBelow ; prAbove = prAbove } = <WellDefined reflexive (symmetric (transitive (symmetric +Associative) identLeft)) (ringCanCancelPositive (0<n prAbove) (<WellDefined prBelow (symmetric (transitive *DistributesOver+' (+WellDefined (transitive (symmetric *Associative) (transitive *Commutative (transitive (*WellDefined 1/npr reflexive) identIsIdent))) identIsIdent))) (<WellDefined identLeft groupIsAbelian (orderRespectsAddition (0<n prAbove) (fromN x)))))
|
||||
approximationIsNear 1/n 1/npr a 0<a a<1 (succ m) with computeFloor' 0 (Semiring.sumZeroRight ℕSemiring n) (a * fromN n) (0<aFromN 0<a) (<WellDefined reflexive identIsIdent (ringCanMultiplyByPositive (0<n 0<a) a<1))
|
||||
... | x , record { prBelow = inl prBelow ; prAbove = prAbove } = <WellDefined reflexive (+WellDefined (symmetric (partialSums'Translate 0G (fromN x * 1/n) _ m)) reflexive) (ringCanCancelPositive (0<n prAbove) (<WellDefined reflexive (transitive (+WellDefined (transitive (+WellDefined (transitive (transitive (symmetric identIsIdent) (transitive *Commutative (*WellDefined reflexive (symmetric 1/npr))) ) *Associative) *Commutative) (symmetric *DistributesOver+')) (transitive (transitive (transitive (symmetric identIsIdent) (*WellDefined (transitive (symmetric 1/npr) *Commutative) reflexive)) (symmetric *Associative)) *Commutative)) (symmetric *DistributesOver+')) (<WellDefined reflexive (+WellDefined (+WellDefined reflexive (transitive (partialSums'WellDefined' _ _ _ (λ m → applyWellDefined _ _ _ dot (λ {_} {_} {s} → dotWellDefined {_} {_} {s}) (λ m → powerSeqWellDefined reflexive (transitive (transitive (transitive (symmetric identIsIdent) *Commutative) (*WellDefined reflexive (symmetric 1/npr))) *Associative) m) m) m) (symmetric (lemma2 (fromN n) 0G 1/n (1/n * 1/n) _ m)))) reflexive) (<WellDefined reflexive (+WellDefined (+WellDefined reflexive (partialSums'WellDefined _ _ (symmetric timesZero) _ m)) reflexive) (<WellDefined reflexive +Associative u)))))
|
||||
where
|
||||
t : ((a * fromN n) + inverse (fromN x)) < ((index (partialSums' 0R (apply dot (powerSeq 1/n 1/n) (baseNExpansion ((a * fromN n) + inverse (fromN x)) (moveInequality prBelow) _))) m) + pow m 1/n)
|
||||
t = approximationIsNear 1/n 1/npr ((a * fromN n) + inverse (fromN x)) (moveInequality prBelow) (<WellDefined reflexive (transitive (transitive (symmetric +Associative) (+WellDefined reflexive invRight)) identRight) (orderRespectsAddition prAbove (inverse (fromN x)))) m
|
||||
u : (a * fromN n) < (fromN x + ((index (partialSums' 0R (apply dot (powerSeq 1/n 1/n) (baseNExpansion ((a * fromN n) + inverse (fromN x)) (moveInequality prBelow) _))) m) + pow m 1/n))
|
||||
u = <WellDefined (transitive (transitive (symmetric +Associative) (+WellDefined reflexive invLeft)) identRight) groupIsAbelian (orderRespectsAddition t (fromN x))
|
||||
... | x , record { prBelow = inr prBelow ; prAbove = prAbove } = <WellDefined reflexive (+WellDefined (symmetric (partialSums'Translate 0G (fromN x * 1/n) _ m)) reflexive) (ringCanCancelPositive (0<n prAbove) (<WellDefined reflexive (transitive (+WellDefined (transitive (+WellDefined (transitive (transitive (symmetric identIsIdent) (transitive *Commutative (*WellDefined reflexive (symmetric 1/npr))) ) *Associative) *Commutative) (symmetric *DistributesOver+')) (transitive (transitive (transitive (symmetric identIsIdent) (*WellDefined (transitive (symmetric 1/npr) *Commutative) reflexive)) (symmetric *Associative)) *Commutative)) (symmetric *DistributesOver+')) (<WellDefined reflexive (+WellDefined (+WellDefined reflexive (transitive (partialSums'WellDefined' _ _ _ (λ m → applyWellDefined _ _ _ dot (λ {_} {_} {s} → dotWellDefined {_} {_} {s}) (λ m → powerSeqWellDefined reflexive (transitive (transitive (transitive (symmetric identIsIdent) *Commutative) (*WellDefined reflexive (symmetric 1/npr))) *Associative) m) m) m) (symmetric (lemma2 (fromN n) 0G 1/n (1/n * 1/n) _ m)))) reflexive) (<WellDefined reflexive (+WellDefined (+WellDefined reflexive (partialSums'WellDefined _ _ (symmetric timesZero) _ m)) reflexive) (<WellDefined reflexive +Associative (<WellDefined (transitive identLeft prBelow) groupIsAbelian (orderRespectsAddition (<WellDefined reflexive (transitive (symmetric identLeft) (+WellDefined (symmetric (transitive (partialSums'WellDefined' 0R _ (constSequence 0R) (λ m → transitive (multiplyZeroSequence _ m) (identityOfIndiscernablesLeft _∼_ reflexive (indexAndConst 0G m))) m ) (transitive (partialSumsConst _ _ m) (transitive identLeft timesZero')))) reflexive)) (powPos m {1/n} (reciprocalPositive _ _ (0<n 0<a) (transitive *Commutative 1/npr)))) (fromN x))))))))
|
||||
|
||||
@@ -13,6 +13,7 @@ open import Rings.Orders.Partial.Definition
|
||||
open import Numbers.Naturals.Semiring
|
||||
open import Numbers.Naturals.Order
|
||||
open import Orders.Total.Definition
|
||||
open import Rings.IntegralDomains.Definition
|
||||
|
||||
module Rings.Orders.Total.Lemmas {n m p : _} {A : Set n} {S : Setoid {n} {m} A} {_+_ : A → A → A} {_*_ : A → A → A} {R : Ring S _+_ _*_} {_<_ : Rel {_} {p} A} {pOrder : SetoidPartialOrder S _<_} {pOrderRing : PartiallyOrderedRing R pOrder} (order : TotallyOrderedRing pOrderRing) where
|
||||
|
||||
@@ -382,3 +383,16 @@ reciprocal<1 a b 0<a ab=1 with totality b 1R
|
||||
... | inl (inl x) = x
|
||||
... | inr b=1 = exFalso (irreflexive (<WellDefined (symmetric ab=1) (transitive (symmetric identIsIdent) (transitive *Commutative ((*WellDefined reflexive (symmetric b=1))))) 0<a))
|
||||
... | inl (inr x) = exFalso (irreflexive (<WellDefined identIsIdent ab=1 (ringMultiplyPositives (0<1 (anyComparisonImpliesNontrivial 0<a)) (0<1 (anyComparisonImpliesNontrivial 0<a)) 0<a x)))
|
||||
|
||||
isIntDom : (nonempty : 1R ∼ 0R → False) → IntegralDomain R
|
||||
IntegralDomain.intDom (isIntDom n) {a} {b} ab=0 a!=0 with totality 0R b
|
||||
... | inr 0=b = symmetric 0=b
|
||||
IntegralDomain.intDom (isIntDom n) {a} {b} ab=0 a!=0 | inl (inl 0<b) with totality 0R a
|
||||
... | inl (inl x) = exFalso (irreflexive (<WellDefined reflexive ab=0 (orderRespectsMultiplication x 0<b)))
|
||||
... | inl (inr x) = exFalso (irreflexive (<WellDefined ab=0 timesZero' (ringCanMultiplyByPositive 0<b x)))
|
||||
... | inr x = exFalso (a!=0 (symmetric x))
|
||||
IntegralDomain.intDom (isIntDom n) {a} {b} ab=0 a!=0 | inl (inr b<0) with totality 0R a
|
||||
... | inl (inl x) = exFalso (irreflexive (<WellDefined (transitive *Commutative ab=0) timesZero' (ringCanMultiplyByPositive x b<0)))
|
||||
... | inl (inr x) = exFalso (irreflexive (<WellDefined reflexive (transitive twoNegativesTimes ab=0) (orderRespectsMultiplication (lemm2 a x) (lemm2 b b<0))))
|
||||
... | inr x = exFalso (a!=0 (symmetric x))
|
||||
IntegralDomain.nontrivial (isIntDom n) = n
|
||||
|
||||
Reference in New Issue
Block a user