### Nuprl Lemma : partition-refinement-sum

`∀I:Interval`
`  (icompact(I)`
`  `` (∀f:I ⟶ℝ. ∀mc:f[x] continuous for x ∈ I. ∀q:partition(I). ∀n:ℕ+.`
`        ((partition-mesh(I;q) ≤ (mc 1 n))`
`        `` frs-increasing(q)`
`        `` (∀p:partition(I). ∀x:partition-choice(full-partition(I;p)). ∀y:partition-choice(full-partition(I;q)).`
`              (p refines q`
`              `` (|partition-sum(f;y;full-partition(I;q)) - partition-sum(f;x;full-partition(I;p))| ≤ ((r1/r(n))`
`                 * |I|)))))))`

Proof

Definitions occuring in Statement :  continuous: `f[x] continuous for x ∈ I` partition-refines: `P refines Q` partition-sum: `partition-sum(f;x;p)` partition-choice: `partition-choice(p)` partition-mesh: `partition-mesh(I;p)` full-partition: `full-partition(I;p)` partition: `partition(I)` frs-increasing: `frs-increasing(p)` icompact: `icompact(I)` rfun: `I ⟶ℝ` i-length: `|I|` interval: `Interval` rdiv: `(x/y)` rleq: `x ≤ y` rabs: `|x|` rsub: `x - y` rmul: `a * b` int-to-real: `r(n)` nat_plus: `ℕ+` so_apply: `x[s]` all: `∀x:A. B[x]` implies: `P `` Q` apply: `f a` natural_number: `\$n`
Definitions unfolded in proof :  all: `∀x:A. B[x]` implies: `P `` Q` member: `t ∈ T` continuous: `f[x] continuous for x ∈ I` squash: `↓T` uall: `∀[x:A]. B[x]` prop: `ℙ` true: `True` subtype_rel: `A ⊆r B` uimplies: `b supposing a` guard: `{T}` iff: `P `⇐⇒` Q` and: `P ∧ Q` rev_implies: `P `` Q` so_lambda: `λ2x.t[x]` so_apply: `x[s]` rfun: `I ⟶ℝ` nat_plus: `ℕ+` rneq: `x ≠ y` or: `P ∨ Q` rless: `x < y` sq_exists: `∃x:{A| B[x]}` decidable: `Dec(P)` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` false: `False` not: `¬A` top: `Top` cand: `A c∧ B` label: `...\$L... t` nat: `ℕ` ge: `i ≥ j ` rleq: `x ≤ y` rnonneg: `rnonneg(x)` le: `A ≤ B` int_seg: `{i..j-}` lelt: `i ≤ j < k` partition: `partition(I)` less_than: `a < b` less_than': `less_than'(a;b)` subinterval: `I ⊆ J ` icompact: `icompact(I)` cons: `[a / b]` full-partition: `full-partition(I;p)` partition-choice: `partition-choice(p)` append: `as @ bs` so_lambda: `so_lambda(x,y,z.t[x; y; z])` so_apply: `x[s1;s2;s3]` subtract: `n - m` select: `L[n]` rbetween: `x≤y≤z` sq_stable: `SqStable(P)` partition-sum: `partition-sum(f;x;p)` sq_type: `SQType(T)` i-length: `|I|` uiff: `uiff(P;Q)` rev_uimplies: `rev_uimplies(P;Q)` rge: `x ≥ y` pointwise-req: `x[k] = y[k] for k ∈ [n,m]` frs-non-dec: `frs-non-dec(L)` rsub: `x - y` pointwise-rleq: `x[k] ≤ y[k] for k ∈ [n,m]` int_upper: `{i...}` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` ifthenelse: `if b then t else f fi ` bfalse: `ff` bnot: `¬bb` assert: `↑b` l_all: `(∀x∈L.P[x])` frs-increasing: `frs-increasing(p)` nil: `[]` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` left-endpoint: `left-endpoint(I)` endpoints: `endpoints(I)` rccint: `[l, u]` outl: `outl(x)` pi1: `fst(t)` right-endpoint: `right-endpoint(I)` pi2: `snd(t)`
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut sqequalHypSubstitution applyEquality hypothesisEquality dependent_set_memberEquality thin lambdaEquality imageElimination lemma_by_obid isectElimination because_Cache hypothesis dependent_functionElimination independent_functionElimination natural_numberEquality sqequalRule imageMemberEquality baseClosed equalityTransitivity equalitySymmetry independent_isectElimination productElimination productEquality functionEquality universeEquality setElimination rename inrFormation unionElimination dependent_pairFormation int_eqEquality intEquality isect_memberEquality voidElimination voidEquality independent_pairFormation computeAll setEquality introduction intWeakElimination independent_pairEquality minusEquality axiomEquality hypothesis_subsumption addEquality promote_hyp equalityElimination substitution instantiate equalityEquality pointwiseFunctionality baseApply closedConclusion inlFormation cumulativity

Latex:
\mforall{}I:Interval
(icompact(I)
{}\mRightarrow{}  (\mforall{}f:I  {}\mrightarrow{}\mBbbR{}.  \mforall{}mc:f[x]  continuous  for  x  \mmember{}  I.  \mforall{}q:partition(I).  \mforall{}n:\mBbbN{}\msupplus{}.
((partition-mesh(I;q)  \mleq{}  (mc  1  n))
{}\mRightarrow{}  frs-increasing(q)
{}\mRightarrow{}  (\mforall{}p:partition(I).  \mforall{}x:partition-choice(full-partition(I;p)).
\mforall{}y:partition-choice(full-partition(I;q)).
(p  refines  q
{}\mRightarrow{}  (|partition-sum(f;y;full-partition(I;q))
-  partition-sum(f;x;full-partition(I;p))|  \mleq{}  ((r1/r(n))  *  |I|)))))))

Date html generated: 2016_05_18-AM-10_38_53
Last ObjectModification: 2016_01_17-AM-00_58_14

Theory : reals

Home Index