(def-theory-ensemble-instances metric-spaces (target-theories fixed-interval-theory h-o-real-arithmetic) force-under-quick-load (permutations (0) (0 1)) (theory-interpretation-check using-simplification) (sorts (pp ii rr)) (constants (dist"lambda(x,y:ii, abs(x-y))""lambda(x,y:rr, abs(x-y))")) (special-renamings (continuous%at%point ii%continuous%at%point) (continuous ii%continuous)))

(def-theory-ensemble-instances metric-spaces (target-theories fixed-interval-theory) force-under-quick-load (permutations (0)) (theory-interpretation-check using-simplification) (sorts (pp ii)) (constants (dist"lambda(x,y:ii, abs(x-y))")))

(def-theory-ensemble-overloadings metric-spaces (1 2))

(def-theorem sup-property-of-continuityRemark: This entry is multiply defined. See: [1] [2]"forall(f:[ii,rr],x,a:rr,s:sets[ii], total_q{f,[ii,rr]} and ii%continuous(f) and #(sup(s),ii) and forall(x:rr,x in s implies f(x)<=a) implies f(sup(s))<=a)"(theory fixed-interval-theory) (proof ( (apply-macete-with-minor-premises tr%eps-delta-characterization-of-continuity) (unfold-single-defined-constant (0) ii%continuous%at%point) direct-and-antecedent-inference-strategy (instantiate-universal-antecedent"with(p:prop,forall(x:ii,forall(eps:rr,p)));"("sup(s)")) (contrapose"with(p:prop, forall(eps:rr,0<eps implies forsome(delta:rr,p)));") (instantiate-existential ("(f(sup(s))-a)/2")) simplify (cut-with-single-formula"forsome(x:ii, x in s and sup(s)-delta_$0<x)") (antecedent-inference"with(p:prop,forsome(x:ii,p));") (instantiate-existential ("x")) (apply-macete-with-minor-premises absolute-value-non-negative) simplify (apply-macete-with-minor-premises tr%minorizes-property-of-prec%sup) direct-inference (instantiate-existential ("x")) simplify (cut-with-single-formula"f(x)<=a") (move-to-sibling 1) simplify (apply-macete-with-minor-premises absolute-value-non-negative) simplify (cut-with-single-formula"forsome(x:rr,x in s and sup(s)-delta_$0<x)") (antecedent-inference"with(p:prop,forsome(x:rr,p));") (instantiate-existential ("with(x:rr, x)")) (apply-macete-with-minor-premises sup-minus-epsilon-corollary) direct-and-antecedent-inference-strategy )))

(def-theorem subset-of-interval-characterization"forall(s:sets[rr],a,b:ii, forall(x:rr,x in s implies a<=x and x<=b) implies #(s,sets[ii]))"(theory fixed-interval-theory) (proof ( direct-and-antecedent-inference-strategy sort-definedness direct-and-antecedent-inference-strategy (apply-macete-with-minor-premises interval-characterization) (instantiate-existential ("b""a")) simplify simplify )))

(def-theorem inf-lemma"forall(x,y,z:rr, forall(y_0:rr, y<y_0 implies x<=y_0*z) implies x<=y*z)"lemma (theory h-o-real-arithmetic) (proof ( direct-and-antecedent-inference-strategy (cut-with-single-formula"z<=0 or 0<z") (block (script-comment"node added by `cut-with-single-formula' at (0)") (antecedent-inference"with(p:prop,p or p);") (block (script-comment"node added by `antecedent-inference' at (0)") (cut-with-single-formula"x<=(y+1)*z and (y+1)*z<=y*z") simplify (block (script-comment"node added by `cut-with-single-formula' at (1)") direct-and-antecedent-inference-strategy (block (script-comment"node added by `direct-and-antecedent-inference-strategy' at (0)") (backchain"with(p:prop,forall(y_0:rr,p));") simplify) simplify)) (block (script-comment"node added by `antecedent-inference' at (1)") (cut-with-single-formula"y<x/z or x/z<=y") (block (script-comment"node added by `cut-with-single-formula' at (0)") (antecedent-inference"with(p:prop,p or p);") (block (script-comment"node added by `antecedent-inference' at (0)") (instantiate-universal-antecedent"with(p:prop,forall(y_0:rr,p));"("[1/2]*(y+x/z)")) (block (script-comment"node added by `instantiate-universal-antecedent' at (0 0 0)") (contrapose"with(p:prop,not(p));") simplify) (block (script-comment"node added by `instantiate-universal-antecedent' at (0 0 1)") (incorporate-antecedent"with(r,x:rr,x<=r);") (apply-macete-with-minor-premises fractional-expression-manipulation) simplify)) (block (script-comment"node added by `antecedent-inference' at (1)") (incorporate-antecedent"with(y,r:rr,r<=y);") (apply-macete-with-minor-premises fractional-expression-manipulation))) simplify)) simplify )))

(def-constant ii%locally%lipschitz%bound"lambda(phi:[ii,pp], r:rr, 0<r and forall(x,z:ii, x<z implies forsome(y:ii, x<y and y<=z and dist(phi(y),phi(x))<=r*(y-x))))"(theory mappings-from-an-interval))

(def-theorem lipschitz-on-interval-characterization"forall(phi:[ii,pp], r:rr, 0<r and forall(x,y:ii, y<=x implies dist(phi(x),phi(y))<=r*(x-y)) implies lipschitz%bound(phi,r))"lemma (proof ( (while (progresses? unfold-directly-defined-constants) (skip)) direct-and-antecedent-inference-strategy (case-split ("0<=x_$0-y_$0")) (let-script instantiate-antecedents 2 ( (instantiate-universal-antecedent"with(p:prop,forall(x,y:ii,p));"($1 $2)) (simplify-antecedent"with(p:prop,not(p));") simplify)) ($instantiate-antecedents"x_$0""y_$0") ($instantiate-antecedents"y_$0""x_$0") )) (theory mappings-from-an-interval))

(def-theorem continuity-of-dist-expression"forall(phi:[ii,pp],y:ii,a,b:rr, total_q{phi,[ii,pp]} and continuous(phi) implies continuous(lambda(z:ii,a+b*z+dist(phi(z),phi(y)))))"(theory mappings-from-an-interval) (proof ( direct-and-antecedent-inference-strategy (incorporate-antecedent"with(phi:[ii,pp],continuous(phi));") (apply-macete-with-minor-premises tr%eps-delta-characterization-of-continuity) (move-to-sibling 1) simplify-insistently direct-and-antecedent-inference-strategy (apply-macete-with-minor-premises polynomial-continuity-macete) (incorporate-antecedent"with(phi:[ii,pp],forall(x:ii,continuous%at%point(phi,x)));") unfold-defined-constants direct-and-antecedent-inference-strategy (instantiate-existential ("eps")) (instantiate-universal-antecedent"with(p:prop,forall(x:ii,forall(eps:rr,p)));"("x")) (instantiate-universal-antecedent"with(p:pp,r:rr, forall(eps:rr, 0<eps implies forsome(delta:rr, 0<delta and forall(y:ii,abs(r)<=delta implies dist(p,p)<=eps))));"("eps_$0")) (instantiate-existential ("delta")) (cut-with-single-formula"abs(dist(phi(x),phi(y))-dist(phi(y_$0),phi(y)))<=dist(phi(x),phi(y_$0))") (move-to-sibling 1) (apply-macete-with-minor-premises dist-continuity-lemma) (instantiate-universal-antecedent"with(eps_$0,delta,r:rr, forall(y:ii,r<=delta implies r<=eps_$0));"("y_$0")) simplify )))

(def-theorem locally-lipschitz-implies-lipschitz"forall(phi:[ii,pp],r:rr, total_q{phi,[ii,pp]} and continuous(phi) and ii%locally%lipschitz%bound(phi,r) implies lipschitz%bound(phi,r))"lemma (proof ( (apply-macete-with-minor-premises lipschitz-on-interval-characterization) (apply-macete-with-minor-premises tr%eps-delta-characterization-of-continuity) (unfold-single-defined-constant (0) ii%locally%lipschitz%bound) direct-and-antecedent-inference-strategy (cut-with-single-formula"forall(z:rr, y<=z and z<=x implies lambda(x:rr,dist(phi(x),phi(y))-r*(x-y)<=0)(z))") (block (script-comment"node added by `cut-with-single-formula' at (0)") (instantiate-universal-antecedent"with(p:prop,forall(z:rr,p implies p));"("x")) (simplify-antecedent"with(p:prop,not(p));") simplify) (block (script-comment"node added by `cut-with-single-formula' at (1)") (apply-macete-with-minor-premises tr%induction-principle-for-cpos) beta-reduce-repeatedly direct-and-antecedent-inference-strategy simplify (move-to-ancestor 2) (block (script-comment"node added by `direct-and-antecedent-inference-strategy' at (1 0 0)") simplify-insistently direct-and-antecedent-inference-strategy (cut-with-single-formula"#(sup(t_$0)) and y<=sup(t_$0) and sup(t_$0)<=x ") (move-to-sibling 1) (block (script-comment"node added by `cut-with-single-formula' at (1)") direct-and-antecedent-inference-strategy (block (script-comment"node added by `direct-and-antecedent-inference-strategy' at (0)") (apply-macete-with-minor-premises tr%prec%sup-defined) direct-and-antecedent-inference-strategy auto-instantiate-existential (block (script-comment"node added by `direct-and-antecedent-inference-strategy' at (1 0)") (unfold-single-defined-constant (0) majorizes) (instantiate-existential ("x")) simplify)) (block (script-comment"node added by `direct-and-antecedent-inference-strategy' at (1)") (apply-macete-with-minor-premises tr%minorizes-property-of-prec%sup) direct-and-antecedent-inference-strategy (instantiate-existential ("y")) simplify) (block (script-comment"node added by `direct-and-antecedent-inference-strategy' at (2)") (apply-macete-with-minor-premises tr%lub-property-of-prec%sup) direct-and-antecedent-inference-strategy (unfold-single-defined-constant (0) majorizes) direct-and-antecedent-inference-strategy simplify)) (block (script-comment"node added by `cut-with-single-formula' at (0)") (cut-with-single-formula"lambda(z:ii,r*y+([-1]*r)*z+dist(phi(z),phi(y)))(sup(t_$0))<=0") simplify (block (script-comment"node added by `cut-with-single-formula' at (1)") (apply-macete-with-minor-premises sup-property-of-continuity) (block (script-comment"node added by `apply-macete-with-minor-premises' at (0)") direct-and-antecedent-inference-strategy simplify-insistently (block (script-comment"node added by `direct-and-antecedent-inference-strategy' at (1)") (apply-macete-with-minor-premises continuity-of-dist-expression) direct-and-antecedent-inference-strategy (apply-macete-with-minor-premises tr%eps-delta-characterization-of-continuity)) (block (script-comment"node added by `direct-and-antecedent-inference-strategy' at (2)") (apply-macete-with-minor-premises interval-characterization) (instantiate-existential ("x""y"))) (block (script-comment"node added by `direct-and-antecedent-inference-strategy' at (3 0 0)") beta-reduce-with-minor-premises (move-to-sibling 1) (block (script-comment"node added by `beta-reduce-with-minor-premises' at (1)") (apply-macete-with-minor-premises interval-characterization) (instantiate-existential ("x""y")) simplify simplify) simplify)) (block (script-comment"node added by `apply-macete-with-minor-premises' at (1)") (apply-macete-with-minor-premises subset-of-interval-characterization) (instantiate-existential ("x""y")) simplify simplify)))) (block (script-comment"node added by `direct-and-antecedent-inference-strategy' at (1 1 0 0 0)") (instantiate-universal-antecedent"with(p:prop,forall(x,z:ii,p));"("y_$1""z_$0")) (simplify-antecedent"with(z_$0,y_$1:rr,not(y_$1<z_$0));") (block (script-comment"node added by `instantiate-universal-antecedent' at (0 0 1 0 0)") (instantiate-existential ("y_$0")) (block (script-comment"node added by `instantiate-existential' at (0 0)") (cut-with-single-formula"dist(phi(y_$0),phi(y))<=dist(phi(y_$0),phi(y_$1))+dist(phi(y_$1),phi(y))") (move-to-sibling 1) (apply-macete-with-minor-premises triangle-inequality-for-distance) simplify) simplify simplify) (block (script-comment"node added by `instantiate-universal-antecedent' at (1 2)") (apply-macete-with-minor-premises interval-characterization) (instantiate-existential ("x""y")) simplify))) )) (theory mappings-from-an-interval))

(def-theorem locally-lipschitz-implies-lipschitz-plus"forall(phi:[ii,pp], r_0:rr, 0<r_0 and total_q{phi,[ii,pp]} and continuous(phi) and forall(r:rr,r_0<r implies ii%locally%lipschitz%bound(phi,r)) implies lipschitz%bound(phi,r_0))"(theory mappings-from-an-interval) (usages transportable-macete) (proof ( direct-and-antecedent-inference-strategy (cut-with-single-formula"forall(r:rr,r_0<r implies lipschitz%bound(phi,r))") (incorporate-antecedent"with(phi:[ii,pp],r_0:rr, forall(r:rr,r_0<r implies lipschitz%bound(phi,r)));") unfold-defined-constants unfold-defined-constants direct-and-antecedent-inference-strategy (apply-macete-with-minor-premises inf-lemma) direct-and-antecedent-inference-strategy (backchain"with(p:prop, forall(r:rr, r_0<r implies 0<r and p))") direct-and-antecedent-inference-strategy (apply-macete-with-minor-premises locally-lipschitz-implies-lipschitz) direct-and-antecedent-inference-strategy (backchain"with(p:prop, forall(r:rr, r_0<r implies p))") )))