|
(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
--> --------------------
¤ Dauer der Verarbeitung: 0.65 Sekunden
(vorverarbeitet)
¤
|
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.
|
