Step
*
8
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,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))
BY
{ ((Assert t ∈ {s:ℝ| (r0 ≤ s) ∧ (r0 < (r + s))} BY
(DSetVars THEN MemTypeCD THEN Auto THEN (Assert r0 < r BY Auto) THEN RWO "-2<" 0 THEN Auto))
THEN (Assert s ∈ {s:ℝ| (r0 ≤ s) ∧ (r0 < (r + s))} BY
(DSetVars THEN MemTypeCD THEN Auto THEN (Assert r0 < r BY Auto) THEN RWO "-2<" 0 THEN Auto))
) }
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. ∀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}
17. t ∈ {s:ℝ| (r0 ≤ s) ∧ (r0 < (r + s))}
18. s ∈ {s:ℝ| (r0 ≤ s) ∧ (r0 < (r + s))}
⊢ (f convex-comb(g a;g b;r;s)) < (f convex-comb(g a;g b;r;t))
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. \mforall{}x,y:\{x:\mBbbR{}| x \mmember{} I\} . \mforall{}r:\{r:\mBbbR{}| r0 \mleq{} r\} . \mforall{}s:\{s:\mBbbR{}| (r0 \mleq{} s) \mwedge{} (r0 < (r + s))\} . \mforall{}X,Y:\{x:\mBbbR{}| x \mmember{} I\} .
\mforall{}R:\{R:\mBbbR{}| (r0 \mleq{} R) \mwedge{} (r0 < (r + R))\} . \mforall{}S:\{S:\mBbbR{}| ((r0 \mleq{} S) \mwedge{} (r0 < (s + S))) \mwedge{} (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:\mBbbR{}| a \mmember{} I\}
13. b : \{b:\mBbbR{}| (b \mmember{} I) \mwedge{} (a < b)\}
14. r : \{r:\mBbbR{}| r0 < r\}
15. s : \{s:\mBbbR{}| r0 \mleq{} s\}
16. t : \{t:\mBbbR{}| s < t\}
\mvdash{} (f convex-comb(g a;g b;r;s)) < (f convex-comb(g a;g b;r;t))
By
Latex:
((Assert t \mmember{} \{s:\mBbbR{}| (r0 \mleq{} s) \mwedge{} (r0 < (r + s))\} BY
(DSetVars THEN MemTypeCD THEN Auto THEN (Assert r0 < r BY Auto) THEN RWO "-2<" 0 THEN Auto))
THEN (Assert s \mmember{} \{s:\mBbbR{}| (r0 \mleq{} s) \mwedge{} (r0 < (r + s))\} BY
(DSetVars
THEN MemTypeCD
THEN Auto
THEN (Assert r0 < r BY
Auto)
THEN RWO "-2<" 0
THEN Auto))
)
Home
Index