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