### Nuprl Lemma : rabs-Riemann-sum

`∀[a:ℝ]. ∀[b:{b:ℝ| a ≤ b} ]. ∀[f:[a, b] ⟶ℝ]. ∀[k:ℕ+].  (|Riemann-sum(f;a;b;k)| ≤ Riemann-sum(λx.|f x|;a;b;k))`

Proof

Definitions occuring in Statement :  Riemann-sum: `Riemann-sum(f;a;b;k)` rfun: `I ⟶ℝ` rccint: `[l, u]` rleq: `x ≤ y` rabs: `|x|` real: `ℝ` nat_plus: `ℕ+` uall: `∀[x:A]. B[x]` set: `{x:A| B[x]} ` apply: `f a` lambda: `λx.A[x]`
Definitions unfolded in proof :  partition-sum: `partition-sum(f;x;p)` default-partition-choice: `default-partition-choice(p)` nat_plus: `ℕ+` uimplies: `b supposing a` so_apply: `x[s]` so_lambda: `λ2x.t[x]` false: `False` not: `¬A` le: `A ≤ B` rnonneg: `rnonneg(x)` rleq: `x ≤ y` squash: `↓T` Riemann-sum: `Riemann-sum(f;a;b;k)` and: `P ∧ Q` iff: `P `⇐⇒` Q` all: `∀x:A. B[x]` implies: `P `` Q` sq_stable: `SqStable(P)` subtype_rel: `A ⊆r B` rfun: `I ⟶ℝ` prop: `ℙ` member: `t ∈ T` uall: `∀[x:A]. B[x]` has-value: `(a)↓` callbyvalueall: callbyvalueall has-valueall: `has-valueall(a)` top: `Top` uiff: `uiff(P;Q)` less_than: `a < b` exists: `∃x:A. B[x]` satisfiable_int_formula: `satisfiable_int_formula(fmla)` or: `P ∨ Q` decidable: `Dec(P)` lelt: `i ≤ j < k` guard: `{T}` int_seg: `{i..j-}` rev_uimplies: `rev_uimplies(P;Q)` rge: `x ≥ y` rsub: `x - y` frs-non-dec: `frs-non-dec(L)`
Lemmas referenced :  equal_wf lelt_wf subtype_rel_list radd-zero-both radd-rminus-both radd_functionality radd-ac radd_comm uiff_transitivity radd-preserves-rleq radd_wf int-to-real_wf rminus_wf full-partition-non-dec rabs-of-nonneg req_weakening rmul_functionality rleq_functionality rleq_weakening_equal rabs-rmul rsum_functionality2 rleq_weakening rabs-rsum rleq_transitivity rleq_functionality_wrt_implies rsum_wf subtract_wf length_wf rmul_wf select_wf int_seg_properties nat_plus_properties decidable__le satisfiable-full-omega-tt intformand_wf intformnot_wf intformle_wf itermConstant_wf itermVar_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_wf decidable__lt add-is-int-iff subtract-is-int-iff intformless_wf itermAdd_wf itermSubtract_wf int_formula_prop_less_lemma int_term_value_add_lemma int_term_value_subtract_lemma false_wf int_seg_wf le_wf list_set_type full-partition_wf full-partition-point-member member_rccint_lemma uniform-partition_wf partition_wf evalall-reduce sq_stable__rleq rabs_wf Riemann-sum_wf rleq_wf subtype_rel_self rfun_wf rccint_wf real_wf i-member_wf rccint-icompact less_than'_wf rsub_wf nat_plus_wf set_wf value-type-has-value set-value-type less_than_wf int-value-type list_wf and_wf valueall-type-has-valueall list-valueall-type set-valueall-type real-valueall-type
Rules used in proof :  equalityEquality lambdaFormation intEquality independent_isectElimination voidElimination isect_memberEquality equalitySymmetry equalityTransitivity axiomEquality natural_numberEquality minusEquality independent_pairEquality imageElimination baseClosed imageMemberEquality productElimination dependent_functionElimination independent_functionElimination setEquality applyEquality lambdaEquality sqequalRule because_Cache hypothesis dependent_set_memberEquality hypothesisEquality isectElimination sqequalHypSubstitution lemma_by_obid rename thin setElimination cut introduction isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution callbyvalueReduce voidEquality closedConclusion baseApply promote_hyp pointwiseFunctionality computeAll independent_pairFormation int_eqEquality dependent_pairFormation unionElimination addEquality productEquality substitution

Latex:
\mforall{}[a:\mBbbR{}].  \mforall{}[b:\{b:\mBbbR{}|  a  \mleq{}  b\}  ].  \mforall{}[f:[a,  b]  {}\mrightarrow{}\mBbbR{}].  \mforall{}[k:\mBbbN{}\msupplus{}].
(|Riemann-sum(f;a;b;k)|  \mleq{}  Riemann-sum(\mlambda{}x.|f  x|;a;b;k))

Date html generated: 2016_05_18-AM-10_40_44
Last ObjectModification: 2016_01_17-AM-00_23_26

Theory : reals

Home Index