Nuprl Lemma : absval_sum

`∀[n:ℕ]. ∀[f:ℕn ⟶ ℤ].  (|Σ(f[x] | x < n)| ≤ Σ(|f[x]| | x < n))`

Proof

Definitions occuring in Statement :  sum: `Σ(f[x] | x < k)` absval: `|i|` int_seg: `{i..j-}` nat: `ℕ` uall: `∀[x:A]. B[x]` so_apply: `x[s]` le: `A ≤ B` function: `x:A ⟶ B[x]` natural_number: `\$n` int: `ℤ`
Definitions unfolded in proof :  rev_uimplies: `rev_uimplies(P;Q)` rev_implies: `P `` Q` iff: `P `⇐⇒` Q` bfalse: `ff` ifthenelse: `if b then t else f fi ` uiff: `uiff(P;Q)` btrue: `tt` it: `⋅` unit: `Unit` bool: `𝔹` or: `P ∨ Q` decidable: `Dec(P)` lelt: `i ≤ j < k` int_seg: `{i..j-}` guard: `{T}` less_than': `less_than'(a;b)` absval: `|i|` le: `A ≤ B` prop: `ℙ` and: `P ∧ Q` top: `Top` not: `¬A` exists: `∃x:A. B[x]` satisfiable_int_formula: `satisfiable_int_formula(fmla)` uimplies: `b supposing a` ge: `i ≥ j ` false: `False` implies: `P `` Q` all: `∀x:A. B[x]` subtype_rel: `A ⊆r B` nat: `ℕ` so_apply: `x[s]` so_lambda: `λ2x.t[x]` member: `t ∈ T` uall: `∀[x:A]. B[x]`
Lemmas referenced :  le_weakening int-triangle-inequality le_functionality int_term_value_add_lemma itermAdd_wf lelt_wf decidable__lt sum_wf equal_wf assert_of_bnot eqff_to_assert iff_weakening_uiff not_wf bnot_wf iff_transitivity assert_of_eq_int eqtt_to_assert assert_wf int_subtype_base equal-wf-base uiff_transitivity bool_wf eq_int_wf primrec-unroll subtype_rel_self int_seg_subtype subtype_rel_dep_function int_term_value_subtract_lemma int_formula_prop_not_lemma itermSubtract_wf intformnot_wf subtract_wf decidable__le int_seg_properties le_wf false_wf primrec0_lemma nat_wf primrec_wf less_than'_wf less_than_wf ge_wf int_formula_prop_wf int_formula_prop_less_lemma int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_le_lemma int_formula_prop_and_lemma intformless_wf itermVar_wf itermConstant_wf intformle_wf intformand_wf satisfiable-full-omega-tt nat_properties absval_wf int_seg_wf sum-as-primrec
Rules used in proof :  impliesFunctionality baseClosed closedConclusion baseApply equalityElimination unionElimination applyLambdaEquality dependent_set_memberEquality minusEquality functionEquality equalitySymmetry equalityTransitivity axiomEquality addEquality independent_pairEquality productElimination independent_functionElimination computeAll independent_pairFormation voidEquality voidElimination isect_memberEquality dependent_functionElimination intEquality int_eqEquality dependent_pairFormation independent_isectElimination intWeakElimination lambdaFormation hypothesis because_Cache rename setElimination natural_numberEquality functionExtensionality applyEquality lambdaEquality hypothesisEquality thin isectElimination sqequalHypSubstitution extract_by_obid sqequalRule cut introduction isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[f:\mBbbN{}n  {}\mrightarrow{}  \mBbbZ{}].    (|\mSigma{}(f[x]  |  x  <  n)|  \mleq{}  \mSigma{}(|f[x]|  |  x  <  n))

Date html generated: 2017_04_14-AM-09_21_48
Last ObjectModification: 2017_04_13-AM-00_46_41

Theory : int_2

Home Index