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

Step * of Lemma quasilinear-weighted-mean-properties

∀I,J:Interval. ∀f:{x:ℝ| x ∈ J}  ⟶ {x:ℝ| x ∈ I} . ∀g:{x:ℝ| x ∈ I}  ⟶ {x:ℝ| x ∈ J} .

  (((∀x1,x2:{x:ℝ| x ∈ J} .  ((x1 < x2) ⇒ ((f x1) < (f x2)))) ∨ (∀x1,x2:{x:ℝ| x ∈ J} .  ((x1 < x2) ⇒ ((f x2) < (f x1)))\000C))
  ⇒ (∀x1,x2:{x:ℝ| x ∈ J} .  ((x1 = x2) ⇒ ((f x1) = (f x2))))
  ⇒ (∀x1,x2:{x:ℝ| x ∈ I} .  ((x1 = x2) ⇒ ((g x1) = (g x2))))
  ⇒ (∀x:{x:ℝ| x ∈ I} . ((f (g x)) = x))
  ⇒ weighted-mean-properties(I;quasilinear-weighted-mean(f;g)))
BY
{ (Auto THEN D 0 THEN Auto THEN RepUR ``quasilinear-weighted-mean`` 0) }

1
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. x : {x:ℝ| x ∈ I}
10. r : {r:ℝ| r0 ≤ r}
11. s : {s:ℝ| (r0 ≤ s) ∧ (r0 < (r + s))}
⊢ (f convex-comb(g x;g x;r;s)) = 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}
10. b : {b:ℝ| (b ∈ I) ∧ (a < b)}
11. r : {r:ℝ| r0 < r}
12. s : {s:ℝ| r0 < s}
⊢ a = (f convex-comb(g a;g b;r1;r0))

3
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}
10. b : {b:ℝ| (b ∈ I) ∧ (a < b)}
11. r : {r:ℝ| r0 < r}
12. s : {s:ℝ| r0 < s}
13. a = (quasilinear-weighted-mean(f;g) a b r1 r0)
⊢ (f convex-comb(g a;g b;r1;r0)) < (f convex-comb(g a;g b;r;s))

4
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}
10. b : {b:ℝ| (b ∈ I) ∧ (a < b)}
11. r : {r:ℝ| r0 < r}
12. s : {s:ℝ| r0 < s}
13. a = (quasilinear-weighted-mean(f;g) a b r1 r0)
14. (quasilinear-weighted-mean(f;g) a b r1 r0) < (quasilinear-weighted-mean(f;g) a b r s)
⊢ (f convex-comb(g a;g b;r;s)) < (f convex-comb(g a;g b;r0;r1))

5
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}
10. b : {b:ℝ| (b ∈ I) ∧ (a < b)}
11. r : {r:ℝ| r0 < r}
12. s : {s:ℝ| r0 < s}
13. a = (quasilinear-weighted-mean(f;g) a b r1 r0)
14. (quasilinear-weighted-mean(f;g) a b r1 r0) < (quasilinear-weighted-mean(f;g) a b r s)
15. (quasilinear-weighted-mean(f;g) a b r s) < (quasilinear-weighted-mean(f;g) a b r0 r1)
⊢ (f convex-comb(g a;g b;r0;r1)) = b

6
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 : {a:ℝ| a ∈ I}
11. b : {b:ℝ| b ∈ I}
12. r : {r:ℝ| r0 < r}
13. s : {s:ℝ| (r0 < s) ∧ (r0 < (r + s))}
14. t : {t:ℝ| r0 < t}
⊢ (f convex-comb(g a;g b;r * t;s * t)) = (f convex-comb(g a;g b;r;s))

7
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))}
⊢ (f 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))
= (f 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))

8
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,y:{x:ℝ| x ∈ I} . ∀r:{r:ℝ| r0 ≤ r} . ∀s:{s:ℝ| (r0 ≤ s) ∧ (r0 < (r + s))} . ∀X,Y:{x:ℝ| x ∈ I} . ∀R:{R:ℝ|

                                                                                                     (r0 ≤ R)

                                                                                                     ∧ (r0 < (r + R))} .

    ∀S:{S:ℝ| ((r0 ≤ S) ∧ (r0 < (s + S))) ∧ (r0 < (R + S))} .
      ((quasilinear-weighted-mean(f;g) (quasilinear-weighted-mean(f;g) x y r s)
        (quasilinear-weighted-mean(f;g) X Y R S)
        (r + s)
        (R + S))
      = (quasilinear-weighted-mean(f;g) (quasilinear-weighted-mean(f;g) x X r R)
         (quasilinear-weighted-mean(f;g) y Y s S)
         (r + R)
         (s + S)))
12. a : {a:ℝ| a ∈ I}
13. b : {b:ℝ| (b ∈ I) ∧ (a < b)}
14. r : {r:ℝ| r0 < r}
15. s : {s:ℝ| r0 ≤ s}
16. t : {t:ℝ| s < t}
⊢ (f convex-comb(g a;g b;r;s)) < (f convex-comb(g a;g b;r;t))

9
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,y:{x:ℝ| x ∈ I} . ∀r:{r:ℝ| r0 ≤ r} . ∀s:{s:ℝ| (r0 ≤ s) ∧ (r0 < (r + s))} . ∀X,Y:{x:ℝ| x ∈ I} . ∀R:{R:ℝ|

                                                                                                     (r0 ≤ R)

                                                                                                     ∧ (r0 < (r + R))} .

12. ∀a:{a:ℝ| a ∈ I} . ∀b:{b:ℝ| (b ∈ I) ∧ (a < b)} . ∀r:{r:ℝ| r0 < r} . ∀s:{s:ℝ| r0 ≤ s} . ∀t:{t:ℝ| s < t} .

((quasilinear-weighted-mean(f;g) a b r s) < (quasilinear-weighted-mean(f;g) a b r t))
13. x : {x:ℝ| x ∈ I}
14. y : {x:ℝ| x ∈ I}
15. z : {z:ℝ| (z ∈ I) ∧ (y < z)}
16. r : {r:ℝ| r0 ≤ r}
17. s : {s:ℝ| r0 < s}
⊢ (f convex-comb(g x;g y;r;s)) < (f convex-comb(g x;g z;r;s))

Latex:

Latex:
\mforall{}I,J:Interval. \mforall{}f:\{x:\mBbbR{}| x \mmember{} J\} {}\mrightarrow{} \{x:\mBbbR{}| x \mmember{} I\} . \mforall{}g:\{x:\mBbbR{}| x \mmember{} I\} {}\mrightarrow{} \{x:\mBbbR{}| x \mmember{} J\} . (((\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))))) {}\mRightarrow{} (\mforall{}x1,x2:\{x:\mBbbR{}| x \mmember{} J\} . ((x1 = x2) {}\mRightarrow{} ((f x1) = (f x2)))) {}\mRightarrow{} (\mforall{}x1,x2:\{x:\mBbbR{}| x \mmember{} I\} . ((x1 = x2) {}\mRightarrow{} ((g x1) = (g x2)))) {}\mRightarrow{} (\mforall{}x:\{x:\mBbbR{}| x \mmember{} I\} . ((f (g x)) = x)) {}\mRightarrow{} weighted-mean-properties(I;quasilinear-weighted-mean(f;g))) By Latex: (Auto THEN D 0 THEN Auto THEN RepUR ``quasilinear-weighted-mean`` 0) Home Index