### Nuprl Lemma : locally-non-constant-deriv-seq-test

`∀a,b:ℝ. ∀f:[a, b] ⟶ℝ. ∀c:ℝ.`
`  ((∀u,v:{v:ℝ| v ∈ [a, b]} .`
`      ((u < v)`
`      `` (∃k:ℕ`
`           ∃F:ℕk + 1 ⟶ [a, b] ⟶ℝ`
`            (finite-deriv-seq([a, b];k;i,x.F[i;x])`
`            ∧ (∀x:{x:ℝ| x ∈ [a, b]} . (F[0;x] = (f(x) - c)))`
`            ∧ (∃z:{z:ℝ| z ∈ [u, v]} . (r0 < Σ{|F[i;z]| | 0≤i≤k}))))))`
`  `` locally-non-constant(f;a;b;c))`

Proof

Definitions occuring in Statement :  finite-deriv-seq: `finite-deriv-seq(I;k;i,x.F[i; x])` locally-non-constant: `locally-non-constant(f;a;b;c)` r-ap: `f(x)` rfun: `I ⟶ℝ` rccint: `[l, u]` i-member: `r ∈ I` rsum: `Σ{x[k] | n≤k≤m}` rless: `x < y` rabs: `|x|` rsub: `x - y` req: `x = y` int-to-real: `r(n)` real: `ℝ` int_seg: `{i..j-}` nat: `ℕ` so_apply: `x[s1;s2]` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` implies: `P `` Q` and: `P ∧ Q` set: `{x:A| B[x]} ` function: `x:A ⟶ B[x]` add: `n + m` natural_number: `\$n`
Definitions unfolded in proof :  all: `∀x:A. B[x]` implies: `P `` Q` member: `t ∈ T` uall: `∀[x:A]. B[x]` prop: `ℙ` exists: `∃x:A. B[x]` nat: `ℕ` and: `P ∧ Q` so_lambda: `λ2x y.t[x; y]` label: `...\$L... t` rfun: `I ⟶ℝ` so_apply: `x[s1;s2]` subtype_rel: `A ⊆r B` int_seg: `{i..j-}` lelt: `i ≤ j < k` le: `A ≤ B` less_than': `less_than'(a;b)` false: `False` not: `¬A` rless: `x < y` sq_exists: `∃x:A [B[x]]` nat_plus: `ℕ+` ge: `i ≥ j ` decidable: `Dec(P)` or: `P ∨ Q` uimplies: `b supposing a` satisfiable_int_formula: `satisfiable_int_formula(fmla)` top: `Top` i-member: `r ∈ I` rccint: `[l, u]` sq_stable: `SqStable(P)` squash: `↓T` so_lambda: `λ2x.t[x]` so_apply: `x[s]` r-ap: `f(x)` locally-non-constant: `locally-non-constant(f;a;b;c)` cand: `A c∧ B` rneq: `x ≠ y` guard: `{T}` iff: `P `⇐⇒` Q` uiff: `uiff(P;Q)` req_int_terms: `t1 ≡ t2`
Lemmas referenced :  i-member_wf rccint_wf rless_wf istype-nat int_seg_wf finite-deriv-seq_wf subtype_rel_self real_wf req_wf istype-false nat_properties nat_plus_properties decidable__lt full-omega-unsat intformand_wf intformnot_wf intformless_wf itermConstant_wf itermAdd_wf itermVar_wf intformle_wf istype-int int_formula_prop_and_lemma istype-void int_formula_prop_not_lemma int_formula_prop_less_lemma int_term_value_constant_lemma int_term_value_add_lemma int_term_value_var_lemma int_formula_prop_le_lemma int_formula_prop_wf istype-le istype-less_than rsub_wf r-ap_wf member_rccint_lemma sq_stable__rleq int-to-real_wf rsum_wf rabs_wf rfun_wf locally-non-zero-finite-deriv-seq radd-preserves-rless rleq_transitivity rleq_wf rneq_wf radd_wf itermSubtract_wf rless_functionality req-iff-rsub-is-0 real_polynomial_null real_term_value_sub_lemma real_term_value_add_lemma real_term_value_var_lemma real_term_value_const_lemma
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation_alt sqequalRule functionIsType setIsType inhabitedIsType hypothesisEquality universeIsType cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesis because_Cache setElimination rename productIsType natural_numberEquality addEquality lambdaEquality_alt applyEquality functionEquality setEquality dependent_set_memberEquality_alt independent_pairFormation dependent_functionElimination unionElimination independent_isectElimination approximateComputation independent_functionElimination dependent_pairFormation_alt int_eqEquality isect_memberEquality_alt voidElimination productElimination imageMemberEquality baseClosed imageElimination inlFormation_alt inrFormation_alt equalityTransitivity equalitySymmetry

Latex:
\mforall{}a,b:\mBbbR{}.  \mforall{}f:[a,  b]  {}\mrightarrow{}\mBbbR{}.  \mforall{}c:\mBbbR{}.
((\mforall{}u,v:\{v:\mBbbR{}|  v  \mmember{}  [a,  b]\}  .
((u  <  v)
{}\mRightarrow{}  (\mexists{}k:\mBbbN{}
\mexists{}F:\mBbbN{}k  +  1  {}\mrightarrow{}  [a,  b]  {}\mrightarrow{}\mBbbR{}
(finite-deriv-seq([a,  b];k;i,x.F[i;x])
\mwedge{}  (\mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  [a,  b]\}  .  (F[0;x]  =  (f(x)  -  c)))
\mwedge{}  (\mexists{}z:\{z:\mBbbR{}|  z  \mmember{}  [u,  v]\}  .  (r0  <  \mSigma{}\{|F[i;z]|  |  0\mleq{}i\mleq{}k\}))))))
{}\mRightarrow{}  locally-non-constant(f;a;b;c))

Date html generated: 2019_10_30-AM-09_11_01
Last ObjectModification: 2018_11_08-PM-01_20_51

Theory : reals

Home Index