Step
*
7
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))}
⊢ (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))
BY
{ ((Assert (r0 ≤ r)
∧ ((r0 ≤ s) ∧ (r0 < (r + s)))
∧ ((r0 ≤ R) ∧ (r0 < (r + R)))
∧ ((r0 ≤ S) ∧ (r0 < (s + S)))
∧ (r0 < (R + S)) BY
(DSetVars THEN Unhide THEN Auto))
THEN ExRepD
THEN (Assert r0 < ((r + s) + R + S) BY
(RWO "-1<" 0 THEN Auto))
THEN (Assert r0 < ((r + R) + s + S) BY
Auto)
THEN BHyp 6
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 : {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)
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))\}
\mvdash{} (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))
By
Latex:
((Assert (r0 \mleq{} r)
\mwedge{} ((r0 \mleq{} s) \mwedge{} (r0 < (r + s)))
\mwedge{} ((r0 \mleq{} R) \mwedge{} (r0 < (r + R)))
\mwedge{} ((r0 \mleq{} S) \mwedge{} (r0 < (s + S)))
\mwedge{} (r0 < (R + S)) BY
(DSetVars THEN Unhide THEN Auto))
THEN ExRepD
THEN (Assert r0 < ((r + s) + R + S) BY
(RWO "-1<" 0 THEN Auto))
THEN (Assert r0 < ((r + R) + s + S) BY
Auto)
THEN BHyp 6
THEN Auto)
Home
Index