Proof of Nuprl Lemma : quasilinear-weighted-mean-properties

Step * 7 1 of Lemma quasilinear-weighted-mean-properties

1. I : Interval
2. J : Interval
3. f : {x:ℝ| x ∈ J}  ⟶ {x:ℝ| x ∈ I}
4. g : {x:ℝ| x ∈ I}  ⟶ {x:ℝ| x ∈ J}
5. (∀x1,x2:{x:ℝ| x ∈ J} .  ((x1 < x2) ⇒ ((f x1) < (f x2)))) ∨ (∀x1,x2:{x:ℝ| x ∈ J} .  ((x1 < x2) ⇒ ((f x2) < (f x1))))
6. ∀x1,x2:{x:ℝ| x ∈ J} .  ((x1 = x2) ⇒ ((f x1) = (f x2)))
7. ∀x1,x2:{x:ℝ| x ∈ I} .  ((x1 = x2) ⇒ ((g x1) = (g x2)))
8. ∀x:{x:ℝ| x ∈ I} . ((f (g x)) = x)
9. ∀a:{a:ℝ| a ∈ I} . ∀b:{b:ℝ| (b ∈ I) ∧ (a < b)} . ∀r,s:{s:ℝ| r0 < s} .
     ((a = (quasilinear-weighted-mean(f;g) a b r1 r0))
     ∧ ((quasilinear-weighted-mean(f;g) a b r1 r0) < (quasilinear-weighted-mean(f;g) a b r s))
     ∧ ((quasilinear-weighted-mean(f;g) a b r s) < (quasilinear-weighted-mean(f;g) a b r0 r1))
     ∧ ((quasilinear-weighted-mean(f;g) a b r0 r1) = b))

10. ∀a,b:{b:ℝ| b ∈ I} . ∀r:{r:ℝ| r0 < r} . ∀s:{s:ℝ| (r0 < s) ∧ (r0 < (r + s))} . ∀t:{t:ℝ| r0 < t} .

      ((quasilinear-weighted-mean(f;g) a b (r * t) (s * t)) = (quasilinear-weighted-mean(f;g) a b r s))

11. x : {x:ℝ| x ∈ I}
12. y : {x:ℝ| x ∈ I}
13. r : {r:ℝ| r0 ≤ r}
14. s : {s:ℝ| (r0 ≤ s) ∧ (r0 < (r + s))}
15. X : {x:ℝ| x ∈ I}
16. Y : {x:ℝ| x ∈ I}
17. R : {R:ℝ| (r0 ≤ R) ∧ (r0 < (r + R))}
18. S : {S:ℝ| ((r0 ≤ S) ∧ (r0 < (s + S))) ∧ (r0 < (R + S))}
19. r0 ≤ r
20. r0 ≤ s
21. r0 < (r + s)
22. r0 ≤ R
23. r0 < (r + R)
24. r0 ≤ S
25. r0 < (s + S)
26. r0 < (R + S)
27. r0 < ((r + s) + R + S)
28. r0 < ((r + R) + s + S)
⊢ convex-comb(g (f convex-comb(g x;g y;r;s));g (f convex-comb(g X;g Y;R;S));r + s;R + S)
= convex-comb(g (f convex-comb(g x;g X;r;R));g (f convex-comb(g y;g Y;s;S));r + R;s + S)
BY
{ Assert ⌜∀x:{x:ℝ| x ∈ J} . ((g (f x)) = x)⌝⋅ }

1
.....assertion.....
1. I : Interval
2. J : Interval
3. f : {x:ℝ| x ∈ J}  ⟶ {x:ℝ| x ∈ I}
4. g : {x:ℝ| x ∈ I}  ⟶ {x:ℝ| x ∈ J}
5. (∀x1,x2:{x:ℝ| x ∈ J} .  ((x1 < x2) ⇒ ((f x1) < (f x2)))) ∨ (∀x1,x2:{x:ℝ| x ∈ J} .  ((x1 < x2) ⇒ ((f x2) < (f x1))))
6. ∀x1,x2:{x:ℝ| x ∈ J} .  ((x1 = x2) ⇒ ((f x1) = (f x2)))
7. ∀x1,x2:{x:ℝ| x ∈ I} .  ((x1 = x2) ⇒ ((g x1) = (g x2)))
8. ∀x:{x:ℝ| x ∈ I} . ((f (g x)) = x)
9. ∀a:{a:ℝ| a ∈ I} . ∀b:{b:ℝ| (b ∈ I) ∧ (a < b)} . ∀r,s:{s:ℝ| r0 < s} .
     ((a = (quasilinear-weighted-mean(f;g) a b r1 r0))
     ∧ ((quasilinear-weighted-mean(f;g) a b r1 r0) < (quasilinear-weighted-mean(f;g) a b r s))
     ∧ ((quasilinear-weighted-mean(f;g) a b r s) < (quasilinear-weighted-mean(f;g) a b r0 r1))
     ∧ ((quasilinear-weighted-mean(f;g) a b r0 r1) = b))

10. ∀a,b:{b:ℝ| b ∈ I} . ∀r:{r:ℝ| r0 < r} . ∀s:{s:ℝ| (r0 < s) ∧ (r0 < (r + s))} . ∀t:{t:ℝ| r0 < t} .

      ((quasilinear-weighted-mean(f;g) a b (r * t) (s * t)) = (quasilinear-weighted-mean(f;g) a b r s))

11. x : {x:ℝ| x ∈ I}
12. y : {x:ℝ| x ∈ I}
13. r : {r:ℝ| r0 ≤ r}
14. s : {s:ℝ| (r0 ≤ s) ∧ (r0 < (r + s))}
15. X : {x:ℝ| x ∈ I}
16. Y : {x:ℝ| x ∈ I}
17. R : {R:ℝ| (r0 ≤ R) ∧ (r0 < (r + R))}
18. S : {S:ℝ| ((r0 ≤ S) ∧ (r0 < (s + S))) ∧ (r0 < (R + S))}
19. r0 ≤ r
20. r0 ≤ s
21. r0 < (r + s)
22. r0 ≤ R
23. r0 < (r + R)
24. r0 ≤ S
25. r0 < (s + S)
26. r0 < (R + S)
27. r0 < ((r + s) + R + S)
28. r0 < ((r + R) + s + S)
⊢ ∀x:{x:ℝ| x ∈ J} . ((g (f x)) = x)

2
1. I : Interval
2. J : Interval
3. f : {x:ℝ| x ∈ J}  ⟶ {x:ℝ| x ∈ I}
4. g : {x:ℝ| x ∈ I}  ⟶ {x:ℝ| x ∈ J}
5. (∀x1,x2:{x:ℝ| x ∈ J} .  ((x1 < x2) ⇒ ((f x1) < (f x2)))) ∨ (∀x1,x2:{x:ℝ| x ∈ J} .  ((x1 < x2) ⇒ ((f x2) < (f x1))))
6. ∀x1,x2:{x:ℝ| x ∈ J} .  ((x1 = x2) ⇒ ((f x1) = (f x2)))
7. ∀x1,x2:{x:ℝ| x ∈ I} .  ((x1 = x2) ⇒ ((g x1) = (g x2)))
8. ∀x:{x:ℝ| x ∈ I} . ((f (g x)) = x)
9. ∀a:{a:ℝ| a ∈ I} . ∀b:{b:ℝ| (b ∈ I) ∧ (a < b)} . ∀r,s:{s:ℝ| r0 < s} .
     ((a = (quasilinear-weighted-mean(f;g) a b r1 r0))
     ∧ ((quasilinear-weighted-mean(f;g) a b r1 r0) < (quasilinear-weighted-mean(f;g) a b r s))
     ∧ ((quasilinear-weighted-mean(f;g) a b r s) < (quasilinear-weighted-mean(f;g) a b r0 r1))
     ∧ ((quasilinear-weighted-mean(f;g) a b r0 r1) = b))

10. ∀a,b:{b:ℝ| b ∈ I} . ∀r:{r:ℝ| r0 < r} . ∀s:{s:ℝ| (r0 < s) ∧ (r0 < (r + s))} . ∀t:{t:ℝ| r0 < t} .

      ((quasilinear-weighted-mean(f;g) a b (r * t) (s * t)) = (quasilinear-weighted-mean(f;g) a b r s))

Latex:

Latex:
1. I : Interval 2. J : Interval 3. f : \{x:\mBbbR{}| x \mmember{} J\} {}\mrightarrow{} \{x:\mBbbR{}| x \mmember{} I\} 4. g : \{x:\mBbbR{}| x \mmember{} I\} {}\mrightarrow{} \{x:\mBbbR{}| x \mmember{} J\} 5. (\mforall{}x1,x2:\{x:\mBbbR{}| x \mmember{} J\} . ((x1 < x2) {}\mRightarrow{} ((f x1) < (f x2)))) \mvee{} (\mforall{}x1,x2:\{x:\mBbbR{}| x \mmember{} J\} . ((x1 < x2) {}\mRightarrow{} ((f x2) < (f x1)))) 6. \mforall{}x1,x2:\{x:\mBbbR{}| x \mmember{} J\} . ((x1 = x2) {}\mRightarrow{} ((f x1) = (f x2))) 7. \mforall{}x1,x2:\{x:\mBbbR{}| x \mmember{} I\} . ((x1 = x2) {}\mRightarrow{} ((g x1) = (g x2))) 8. \mforall{}x:\{x:\mBbbR{}| x \mmember{} I\} . ((f (g x)) = x) 9. \mforall{}a:\{a:\mBbbR{}| a \mmember{} I\} . \mforall{}b:\{b:\mBbbR{}| (b \mmember{} I) \mwedge{} (a < b)\} . \mforall{}r,s:\{s:\mBbbR{}| r0 < s\} . ((a = (quasilinear-weighted-mean(f;g) a b r1 r0)) \mwedge{} ((quasilinear-weighted-mean(f;g) a b r1 r0) < (quasilinear-weighted-mean(f;g) a b r s)) \mwedge{} ((quasilinear-weighted-mean(f;g) a b r s) < (quasilinear-weighted-mean(f;g) a b r0 r1)) \mwedge{} ((quasilinear-weighted-mean(f;g) a b r0 r1) = b)) 10. \mforall{}a,b:\{b:\mBbbR{}| b \mmember{} I\} . \mforall{}r:\{r:\mBbbR{}| r0 < r\} . \mforall{}s:\{s:\mBbbR{}| (r0 < s) \mwedge{} (r0 < (r + s))\} . \mforall{}t:\{t:\mBbbR{}| r0 < t\} . ((quasilinear-weighted-mean(f;g) a b (r * t) (s * t)) = (quasilinear-weighted-mean(f;g) a b r s)) 11. x : \{x:\mBbbR{}| x \mmember{} I\} 12. y : \{x:\mBbbR{}| x \mmember{} I\} 13. r : \{r:\mBbbR{}| r0 \mleq{} r\} 14. s : \{s:\mBbbR{}| (r0 \mleq{} s) \mwedge{} (r0 < (r + s))\} 15. X : \{x:\mBbbR{}| x \mmember{} I\} 16. Y : \{x:\mBbbR{}| x \mmember{} I\} 17. R : \{R:\mBbbR{}| (r0 \mleq{} R) \mwedge{} (r0 < (r + R))\} 18. S : \{S:\mBbbR{}| ((r0 \mleq{} S) \mwedge{} (r0 < (s + S))) \mwedge{} (r0 < (R + S))\} 19. r0 \mleq{} r 20. r0 \mleq{} s 21. r0 < (r + s) 22. r0 \mleq{} R 23. r0 < (r + R) 24. r0 \mleq{} S 25. r0 < (s + S) 26. r0 < (R + S) 27. r0 < ((r + s) + R + S) 28. r0 < ((r + R) + s + S) \mvdash{} convex-comb(g (f convex-comb(g x;g y;r;s));g (f convex-comb(g X;g Y;R;S));r + s;R + S) = convex-comb(g (f convex-comb(g x;g X;r;R));g (f convex-comb(g y;g Y;s;S));r + R;s + S) By Latex: Assert \mkleeneopen{}\mforall{}x:\{x:\mBbbR{}| x \mmember{} J\} . ((g (f x)) = x)\mkleeneclose{}\mcdot{} Home Index