Quelle minkowski_scaf.prf Sprache: Lisp

(minkowski_scaf
(mu_TCC1 0
  (mu_TCC1-1 nil 3477582206
   ("" (typepred "S")
    (("" (expand "sigma_algebra?")
      (("" (flatten)
        (("" (expand "subset_algebra_empty?") (("" (assert) nil nil))
          nil))
        nil))
      nil))
    nil)
   ((subset_algebra_empty? const-decl "bool" subset_algebra_def
     "measure_integration/")
    (finite_emptyset name-judgement "finite_set" finite_sets nil)
    (finite_emptyset name-judgement "finite_set[T]" countable_props
     "sets_aux/")
    (finite_emptyset name-judgement "finite_set[T]" countable_setofsets
     "sets_aux/")
    (member const-decl "bool" sets nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (T formal-type-decl nil minkowski_scaf nil)
    (setof type-eq-decl nil defined_types nil)
    (setofsets type-eq-decl nil sets nil)
    (sigma_algebra? const-decl "bool" subset_algebra_def
     "measure_integration/")
    (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def
     "measure_integration/")
    (S formal-const-decl "sigma_algebra[T]" minkowski_scaf nil))
   nil))
(minkowski_scaf 0
  (minkowski_scaf-1 nil 3477583588
   ("" (skosimp)
    (("" (name "KK" "reals@real_fun_ops_aux[T].max(abs(f!1),abs(g!1))")
      ((""
        (case "forall (x:T): abs(f!1+g!1)(x) <= abs(f!1)(x)+abs(g!1)(x) & abs(f!1)(x)+abs(g!1)(x) <= 2*KK(x)")
        (("1" (case "integrable?(+[T](abs[T](f!1)^p,abs[T](g!1)^p))")
          (("1"
            (lemma "nn_integrable_le"
             ("f" "2^p * (abs[T](f!1) ^ p + abs[T](g!1) ^ p)" "g"
              "abs(f!1 + g!1)^p"))
            (("1" (split -1)
              (("1" (flatten)
                (("1" (lemma "nn_integrable_is_integrable")
                  (("1" (inst - "abs(f!1 + g!1) ^ p")
                    (("1" (rewrite "integral_nn" -3 :dir rl)
                      (("1" (case-replace "p_integrable?(f!1 + g!1)")
                        (("1" (expand "norm")
                          (("1" (typepred "p")
                            (("1" (expand ">=" -1)
                              (("1"
                                (expand "<=" -1)
                                (("1"
                                  (split -1)
                                  (("1"
                                    (name "q" "p/(p-1)")
                                    (("1"
                                      (case "q>1 & 1/p+1/q =1")
                                      (("1"
                                        (flatten -1)
                                        (("1"
                                          (hide -8 -9)
                                          (("1"
                                            (case
                                             "abs(f!1 + g!1) ^ p=(abs(f!1 + g!1) ^(p-1))^q")
                                            (("1"
                                              (name
                                               "H"
                                               "abs(f!1 + g!1) ^ (p - 1)")
                                              (("1"
                                                (replace -1)
                                                (("1"
                                                  (name
                                                   "CH"
                                                   "lambda (x:T): complex_(H(x),0)")
                                                  (("1"
                                                    (case
                                                     "p_integrable?[T,S,mu,p/(p-1)](CH)")
                                                    (("1"
                                                      (case
                                                       "norm[T,S,mu,p / (p - 1)](CH) = norm(f!1+g!1)^(p/q)")
                                                      (("1"
                                                        (lemma
                                                         "holder_scaf[T,S,mu,p,p / (p - 1)]"
                                                         ("f"
                                                          "f!1"
                                                          "g"
                                                          "CH"))
                                                        (("1"
                                                          (lemma
                                                           "holder_scaf[T,S,mu,p,p / (p - 1)]"
                                                           ("f"
                                                            "g!1"
                                                            "g"
                                                            "CH"))
                                                          (("1"
                                                            (replace
                                                             -3)
                                                            (("1"
                                                              (case
                                                               "forall (f:p_integrable[T,S,mu,1]): integral.integrable?(abs(f)) & norm[T, S, mu, 1](f) = integral.integral(abs(f))")
                                                              (("1"
                                                                (inst-cp
                                                                 -
                                                                 "f!1*CH")
                                                                (("1"
                                                                  (inst
                                                                   -
                                                                   "g!1*CH")
                                                                  (("1"
                                                                    (flatten
                                                                     -1)
                                                                    (("1"
                                                                      (case
                                                                       "integral.integral(abs(f!1 * CH)+abs(g!1 * CH)) <= (norm[T, S, mu, p](f!1) + norm[T, S, mu, p](g!1))* norm(f!1 + g!1) ^ (p / q)")
                                                                      (("1"
                                                                        (name
                                                                         "RHS"
                                                                         "norm[T, S, mu, p](f!1) + norm[T, S, mu, p](g!1)")
                                                                        (("1"
                                                                          (replace
                                                                           -1)
                                                                          (("1"
                                                                            (expand
                                                                             "norm"
                                                                             -1)
                                                                            (("1"
                                                                              (replace
                                                                               -1)
                                                                              (("1"
                                                                                (hide
                                                                                 -1)
                                                                                (("1"
                                                                                  (hide
                                                                                   -3
                                                                                   -4
                                                                                   -5
                                                                                   -6
                                                                                   -19
                                                                                   -20)
                                                                                  (("1"
                                                                                    (case
                                                                                     "abs(f!1 + g!1)*H = abs(f!1 + g!1) ^ p")
                                                                                    (("1"
                                                                                      (lemma
                                                                                       "integral_ae_le"
                                                                                       ("f1"
                                                                                        "abs(f!1+g!1)*H"
                                                                                        "f2"
                                                                                        "abs(f!1 * CH) + abs(g!1 * CH)"))
                                                                                      (("1"
                                                                                        (name-replace
                                                                                         "INT"
                                                                                         "integral.integral(abs(f!1 * CH) + abs(g!1 * CH))")
                                                                                        (("1"
                                                                                          (split
                                                                                           -1)
                                                                                          (("1"
                                                                                            (replace
                                                                                             -2)
                                                                                            (("1"
                                                                                              (expand
                                                                                               "norm"
                                                                                               -3)
                                                                                              (("1"
                                                                                                (lemma
                                                                                                 "integral_nonneg"
                                                                                                 ("f"
                                                                                                  "abs(f!1 + g!1) ^ p"))
                                                                                                (("1"
                                                                                                  (split
                                                                                                   -1)
                                                                                                  (("1"
                                                                                                    (name-replace
                                                                                                     "INT2"
                                                                                                     "integral.integral(abs(f!1 + g!1) ^ p)")
                                                                                                    (("1"
                                                                                                      (hide-all-but
                                                                                                       (-1
                                                                                                        -2
                                                                                                        -4
                                                                                                        -11
                                                                                                        -12
                                                                                                        -13
                                                                                                        -14
                                                                                                        1))
                                                                                                      (("1"
                                                                                                        (lemma
                                                                                                         "real_expt_times"
                                                                                                         ("x"
                                                                                                          "INT2"
                                                                                                          "a"
                                                                                                          "1/p"
                                                                                                          "b"
                                                                                                          "p/q"))
                                                                                                        (("1"
                                                                                                          (case-replace
                                                                                                           "1 / p * (p / q)=1/q")
                                                                                                          (("1"
                                                                                                            (replace
                                                                                                             -2
                                                                                                             -5
                                                                                                             rl)
                                                                                                            (("1"
                                                                                                              (case
                                                                                                               "INT2 <= RHS * INT2 ^ (1 / q)")
                                                                                                              (("1"
                                                                                                                (hide
                                                                                                                 -2
                                                                                                                 -3
                                                                                                                 -5
                                                                                                                 -6)
                                                                                                                (("1"
                                                                                                                  (expand
                                                                                                                   ">="
                                                                                                                   -2)
                                                                                                                  (("1"
                                                                                                                    (expand
                                                                                                                     "<="
                                                                                                                     -2)
                                                                                                                    (("1"
                                                                                                                      (split
                                                                                                                       -2)
                                                                                                                      (("1"
                                                                                                                        (lemma
                                                                                                                         "posreal_div_posreal_is_posreal"
                                                                                                                         ("px"
                                                                                                                          "1"
                                                                                                                          "py"
                                                                                                                          "p"))
                                                                                                                        (("1"
                                                                                                                          (lemma
                                                                                                                           "posreal_div_posreal_is_posreal"
                                                                                                                           ("px"
                                                                                                                            "1"
                                                                                                                            "py"
                                                                                                                            "q"))
                                                                                                                          (("1"
                                                                                                                            (lemma
                                                                                                                             "real_expt_plus"
                                                                                                                             ("x"
                                                                                                                              "INT2"
                                                                                                                              "a"
                                                                                                                              "1/p"
                                                                                                                              "b"
                                                                                                                              "1/q"))
                                                                                                                            (("1"
                                                                                                                              (replace
                                                                                                                               -7)
                                                                                                                              (("1"
                                                                                                                                (rewrite
                                                                                                                                 "real_expt_x1"
                                                                                                                                 -1)
                                                                                                                                (("1"
                                                                                                                                  (lemma
                                                                                                                                   "real_expt_pos"
                                                                                                                                   ("px"
                                                                                                                                    "INT2"
                                                                                                                                    "a"
                                                                                                                                    "1/q"))
                                                                                                                                  (("1"
                                                                                                                                    (lemma
                                                                                                                                     "both_sides_times_pos_le1"
                                                                                                                                     ("pz"
                                                                                                                                      "INT2 ^ (1 / q)"
                                                                                                                                      "x"
                                                                                                                                      "INT2 ^ (1 / p)"
                                                                                                                                      "y"
                                                                                                                                      "RHS"))
                                                                                                                                    (("1"
                                                                                                                                      (replace
                                                                                                                                       -3
                                                                                                                                       *
                                                                                                                                       rl)
                                                                                                                                      (("1"
                                                                                                                                        (assert)
                                                                                                                                        nil
                                                                                                                                        nil))
                                                                                                                                      nil)
                                                                                                                                     ("2"
                                                                                                                                      (propax)
                                                                                                                                      nil
                                                                                                                                      nil))
                                                                                                                                    nil)
                                                                                                                                   ("2"
                                                                                                                                    (assert)
                                                                                                                                    nil
                                                                                                                                    nil))
                                                                                                                                  nil))
                                                                                                                                nil))
                                                                                                                              nil))
                                                                                                                            nil))
                                                                                                                          nil))
                                                                                                                        nil)
                                                                                                                       ("2"
                                                                                                                        (replace
                                                                                                                         -1
                                                                                                                         *
                                                                                                                         rl)
                                                                                                                        (("2"
                                                                                                                          (rewrite
                                                                                                                           "real_expt_0x"
                                                                                                                           1)
                                                                                                                          (("1"
                                                                                                                            (expand
                                                                                                                             "RHS")
                                                                                                                            (("1"
                                                                                                                              (assert)
                                                                                                                              nil
                                                                                                                              nil))
                                                                                                                            nil)
                                                                                                                           ("2"
                                                                                                                            (lemma
                                                                                                                             "posreal_div_posreal_is_posreal"
                                                                                                                             ("px"
                                                                                                                              "1"
                                                                                                                              "py"
                                                                                                                              "p"))
                                                                                                                            (("2"
                                                                                                                              (assert)
                                                                                                                              nil
                                                                                                                              nil))
                                                                                                                            nil))
                                                                                                                          nil))
                                                                                                                        nil))
                                                                                                                      nil))
                                                                                                                    nil))
                                                                                                                  nil))
                                                                                                                nil)
                                                                                                               ("2"
                                                                                                                (assert)
                                                                                                                nil
                                                                                                                nil))
                                                                                                              nil))
                                                                                                            nil)
                                                                                                           ("2"
                                                                                                            (assert)
                                                                                                            nil
                                                                                                            nil))
                                                                                                          nil)
                                                                                                         ("2"
                                                                                                          (propax)
                                                                                                          nil
                                                                                                          nil))
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil)
                                                                                                   ("2"
                                                                                                    (skosimp)
                                                                                                    (("2"
                                                                                                      (expand
                                                                                                       "^"
                                                                                                       1)
                                                                                                      (("2"
                                                                                                        (expand
                                                                                                         "abs"
                                                                                                         1)
                                                                                                        (("2"
                                                                                                          (assert)
                                                                                                          nil
                                                                                                          nil))
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil)
                                                                                           ("2"
                                                                                            (hide-all-but
                                                                                             (1
                                                                                              -12
                                                                                              -9
                                                                                              -10
                                                                                              -11
                                                                                              -7
                                                                                              -6
                                                                                              -8))
                                                                                            (("2"
                                                                                              (expand
                                                                                               "ae_le?")
                                                                                              (("2"
                                                                                                (expand
                                                                                                 "pointwise_ae?")
                                                                                                (("2"
                                                                                                  (expand
                                                                                                   "ae?")
                                                                                                  (("2"
                                                                                                    (expand
                                                                                                     "fullset")
                                                                                                    (("2"
                                                                                                      (expand
                                                                                                       "ae_in?")
                                                                                                      (("2"
                                                                                                        (inst
                                                                                                         +
                                                                                                         "emptyset")
                                                                                                        (("2"
                                                                                                          (skosimp)
                                                                                                          (("2"
                                                                                                            (expand
                                                                                                             "member")
                                                                                                            (("2"
                                                                                                              (hide
                                                                                                               1)
                                                                                                              (("2"
                                                                                                                (expand
                                                                                                                 "*"
                                                                                                                 1)
                                                                                                                (("2"
                                                                                                                  (expand
                                                                                                                   "+"
                                                                                                                   1
                                                                                                                   2)
                                                                                                                  (("2"
                                                                                                                    (expand
                                                                                                                     "abs"
                                                                                                                     1)
                                                                                                                    (("2"
                                                                                                                      (expand
                                                                                                                       "+"
                                                                                                                       1)
                                                                                                                      (("2"
                                                                                                                        (replace
                                                                                                                         -1
                                                                                                                         1
                                                                                                                         rl)
                                                                                                                        (("2"
                                                                                                                          (hide
                                                                                                                           -1
                                                                                                                           -3)
                                                                                                                          (("2"
                                                                                                                            (replace
                                                                                                                             -1
                                                                                                                             1
                                                                                                                             rl)
                                                                                                                            (("2"
                                                                                                                              (hide
                                                                                                                               -1)
                                                                                                                              (("2"
                                                                                                                                (simplify
                                                                                                                                 1)
                                                                                                                                (("2"
                                                                                                                                  (expand
                                                                                                                                   "^"
                                                                                                                                   1)
                                                                                                                                  (("2"
                                                                                                                                    (expand
                                                                                                                                     "abs"
                                                                                                                                     1
                                                                                                                                     2)
                                                                                                                                    (("2"
                                                                                                                                      (expand
                                                                                                                                       "+"
                                                                                                                                       1
                                                                                                                                       2)
                                                                                                                                      (("2"
                                                                                                                                        (expand
                                                                                                                                         "abs"
                                                                                                                                         1
                                                                                                                                         4)
                                                                                                                                        (("2"
                                                                                                                                          (expand
                                                                                                                                           "abs"
                                                                                                                                           1
                                                                                                                                           6)
                                                                                                                                          (("2"
                                                                                                                                            (expand
                                                                                                                                             "+ "
                                                                                                                                             1
                                                                                                                                             3)
                                                                                                                                            (("2"
                                                                                                                                              (expand
                                                                                                                                               "+ "
                                                                                                                                               1
                                                                                                                                               5)
                                                                                                                                              (("2"
                                                                                                                                                (rewrite
                                                                                                                                                 "abs_mult"
                                                                                                                                                 1)
                                                                                                                                                (("2"
                                                                                                                                                  (rewrite
                                                                                                                                                   "abs_mult"
                                                                                                                                                   1)
                                                                                                                                                  (("2"
                                                                                                                                                    (typepred
                                                                                                                                                     "abs(f!1(x!1) + g!1(x!1)) ^ (p - 1)")
                                                                                                                                                    (("2"
                                                                                                                                                      (name-replace
                                                                                                                                                       "FGp1"
                                                                                                                                                       "abs(f!1(x!1) + g!1(x!1)) ^ (p - 1)")
                                                                                                                                                      (("2"
                                                                                                                                                        (expand
                                                                                                                                                         "abs"
                                                                                                                                                         1
                                                                                                                                                         3)
                                                                                                                                                        (("2"
                                                                                                                                                          (expand
                                                                                                                                                           "abs"
                                                                                                                                                           1
                                                                                                                                                           4)
                                                                                                                                                          (("2"
                                                                                                                                                            (expand
                                                                                                                                                             "sq_abs")
                                                                                                                                                            (("2"
                                                                                                                                                              (expand
                                                                                                                                                               "Im"
                                                                                                                                                               1)
                                                                                                                                                              (("2"
                                                                                                                                                                (expand
                                                                                                                                                                 "Re"
                                                                                                                                                                 1)
                                                                                                                                                                (("2"
                                                                                                                                                                  (rewrite
                                                                                                                                                                   "sq_0")
                                                                                                                                                                  (("2"
                                                                                                                                                                    (lemma
                                                                                                                                                                     "sqrt_sq")
                                                                                                                                                                    (("2"
                                                                                                                                                                      (inst
                                                                                                                                                                       -
                                                                                                                                                                       "FGp1")
                                                                                                                                                                      (("2"
                                                                                                                                                                        (split)
                                                                                                                                                                        (("1"
                                                                                                                                                                          (replace
                                                                                                                                                                           -1)
                                                                                                                                                                          (("1"
                                                                                                                                                                            (hide
                                                                                                                                                                             -1)
                                                                                                                                                                            (("1"
                                                                                                                                                                              (expand
                                                                                                                                                                               ">="
                                                                                                                                                                               -1)
                                                                                                                                                                              (("1"
                                                                                                                                                                                (expand
                                                                                                                                                                                 "<="
                                                                                                                                                                                 -1)
                                                                                                                                                                                (("1"
                                                                                                                                                                                  (split
                                                                                                                                                                                   -1)
                                                                                                                                                                                  (("1"
                                                                                                                                                                                    (lemma
                                                                                                                                                                                     "both_sides_times_pos_le1"
                                                                                                                                                                                     ("pz"
                                                                                                                                                                                      "FGp1"
                                                                                                                                                                                      "x"
                                                                                                                                                                                      "abs(f!1(x!1) + g!1(x!1))"
                                                                                                                                                                                      "y"
                                                                                                                                                                                      "abs(f!1(x!1))+abs(g!1(x!1))"))
                                                                                                                                                                                    (("1"
                                                                                                                                                                                      (replace
                                                                                                                                                                                       -1
                                                                                                                                                                                       1)
                                                                                                                                                                                      (("1"
                                                                                                                                                                                        (hide
                                                                                                                                                                                         -1
                                                                                                                                                                                         -2)
                                                                                                                                                                                        (("1"
                                                                                                                                                                                          (rewrite
                                                                                                                                                                                           "abs_triangle")
                                                                                                                                                                                          nil
                                                                                                                                                                                          nil))
                                                                                                                                                                                        nil))
                                                                                                                                                                                      nil)
                                                                                                                                                                                     ("2"
                                                                                                                                                                                      (assert)
--> --------------------

--> maximum size reached

--> --------------------

quality90%

¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.31Bemerkung: (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.