Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
complex_integration.summary
Sprache: Unknown
Spracherkennung für: .summary vermutete Sprache: MT940 {MT940[444] Hlasm[1398] Haskell[1780]} [Methode: Schwerpunktbildung, einfache Gewichte, sechs Dimensionen]
***
*** top (22:1:41 11/7/2014)
*** Generated by proveit - ProofLite-6.0.9 (3/14/14)
***
Proof summary for theory top
Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)
Proof summary for theory complex_topology
IMP_metric_space_TCC1.................proved - complete [shostak](0.61 s)
complex_is_complete...................proved - complete [shostak](1.08 s)
Theory totals: 2 formulas, 2 attempted, 2 succeeded (1.68 s)
Proof summary for theory complex_measurable
complex_measurable_TCC1...............proved - complete [shostak](0.09 s)
complex_measurable_def................proved - complete [shostak](0.06 s)
constant_is_complex_measurable........proved - complete [shostak](0.09 s)
scal_complex_measurable...............proved - incomplete [shostak](0.42 s)
sum_complex_measurable................proved - incomplete [shostak](0.08 s)
opp_complex_measurable................proved - incomplete [shostak](0.19 s)
diff_complex_measurable...............proved - incomplete [shostak](-1.99 s)
const_measurable......................proved - complete [shostak](0.07 s)
abs_complex_measurable................proved - incomplete [shostak](0.44 s)
sq_complex_measurable.................proved - incomplete [shostak](0.32 s)
prod_complex_measurable...............proved - incomplete [shostak](0.25 s)
abs_expt_measurable...................proved - incomplete [shostak](0.08 s)
pointwise_complex_measurable..........proved - incomplete [shostak](0.40 s)
Theory totals: 13 formulas, 13 attempted, 13 succeeded (0.49 s)
Proof summary for theory complex_measure_theory
mu_TCC1...............................proved - complete [shostak](0.04 s)
cal_N_TCC1............................proved - complete [shostak](0.13 s)
cal_N_is_measurable...................proved - complete [shostak](0.11 s)
cal_N_def.............................proved - complete [shostak](0.26 s)
Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.54 s)
Proof summary for theory complex_integral
mu_TCC1...............................proved - complete [shostak](0.04 s)
integrable_TCC1.......................proved - incomplete [shostak](0.10 s)
integral_TCC1.........................proved - incomplete [shostak](0.07 s)
integral_TCC2.........................proved - incomplete [shostak](0.07 s)
integrable_def........................proved - complete [shostak](0.07 s)
Re_integral...........................proved - incomplete [shostak](0.07 s)
Im_integral...........................proved - incomplete [shostak](0.07 s)
integrable_is_measurable..............proved - incomplete [shostak](0.08 s)
cal_N_is_measurable...................proved - incomplete [shostak](0.11 s)
integrable_add........................proved - incomplete [shostak](0.42 s)
integrable_scal.......................proved - incomplete [shostak](0.16 s)
integrable_opp........................proved - incomplete [shostak](0.09 s)
integrable_diff.......................proved - incomplete [shostak](0.08 s)
integrable_abs........................proved - incomplete [shostak](0.51 s)
integral_add..........................proved - incomplete [shostak](0.17 s)
integral_scal.........................proved - incomplete [shostak](0.35 s)
integral_opp..........................proved - incomplete [shostak](0.69 s)
integral_diff.........................proved - incomplete [shostak](0.55 s)
integral_abs..........................proved - incomplete [shostak](2.50 s)
Theory totals: 19 formulas, 19 attempted, 19 succeeded (6.19 s)
Proof summary for theory p_integrable_def
mu_TCC1...............................proved - complete [shostak](0.04 s)
p_integrable?_TCC1....................proved - complete [shostak](0.08 s)
p_integrable_TCC1.....................proved - incomplete [shostak](0.17 s)
cal_N_is_p_integrable.................proved - incomplete [shostak](0.17 s)
norm_TCC1.............................proved - incomplete [shostak](0.08 s)
norm_TCC2.............................proved - incomplete [shostak](0.09 s)
norm_TCC3.............................proved - incomplete [shostak](0.13 s)
norm_TCC4.............................proved - incomplete [shostak](0.08 s)
norm_TCC5.............................proved - incomplete [shostak](0.13 s)
norm_eq_0.............................proved - incomplete [shostak](0.35 s)
Theory totals: 10 formulas, 10 attempted, 10 succeeded (1.33 s)
Proof summary for theory young
youngs_aux_TCC1.......................proved - complete [shostak](0.05 s)
youngs_aux............................proved - incomplete [shostak](1.75 s)
youngs_inequality_TCC1................proved - complete [shostak](0.07 s)
youngs_inequality_TCC2................proved - complete [shostak](0.06 s)
youngs_inequality.....................proved - incomplete [shostak](2.14 s)
Theory totals: 5 formulas, 5 attempted, 5 succeeded (4.07 s)
Proof summary for theory holder_scaf
mu_TCC1...............................proved - complete [shostak](0.04 s)
q_TCC1................................proved - complete [shostak](0.03 s)
f_TCC1................................proved - complete [shostak](0.11 s)
g_TCC1................................proved - complete [shostak](0.23 s)
holder_aux............................proved - incomplete [shostak](4.15 s)
holder_judge1.........................proved - incomplete [shostak](0.13 s)
holder_judge2.........................proved - incomplete [shostak](0.22 s)
holder_scaf...........................proved - incomplete [shostak](0.12 s)
Theory totals: 8 formulas, 8 attempted, 8 succeeded (5.02 s)
Proof summary for theory minkowski_scaf
mu_TCC1...............................proved - complete [shostak](0.04 s)
minkowski_scaf........................proved - incomplete [shostak](3.93 s)
Theory totals: 2 formulas, 2 attempted, 2 succeeded (3.97 s)
Proof summary for theory p_integrable
mu_TCC1...............................proved - complete [shostak](0.04 s)
scal_p_integrable.....................proved - incomplete [shostak](0.28 s)
sum_p_integrable......................proved - incomplete [shostak](0.08 s)
opp_p_integrable......................proved - incomplete [shostak](0.10 s)
diff_p_integrable.....................proved - incomplete [shostak](0.31 s)
norm_scal.............................proved - incomplete [shostak](0.45 s)
norm_add..............................proved - incomplete [shostak](0.08 s)
norm_opp..............................proved - incomplete [shostak](0.13 s)
norm_diff.............................proved - incomplete [shostak](0.21 s)
Theory totals: 9 formulas, 9 attempted, 9 succeeded (1.68 s)
Proof summary for theory essentially_bounded
mu_TCC1...............................proved - complete [shostak](0.04 s)
essentially_bounded_TCC1..............proved - complete [shostak](0.16 s)
essential_bound_TCC1..................proved - complete [shostak](0.13 s)
essential_bound_TCC2..................proved - complete [shostak](0.15 s)
essential_bound_def1..................proved - complete [shostak](0.14 s)
essential_bound_def2..................proved - incomplete [shostak](1.46 s)
scal_essentially_bounded..............proved - incomplete [shostak](0.32 s)
add_essentially_bounded...............proved - incomplete [shostak](0.30 s)
opp_essentially_bounded...............proved - incomplete [shostak](0.65 s)
diff_essentially_bounded..............proved - incomplete [shostak](0.16 s)
prod_essentially_bounded..............proved - incomplete [shostak](0.31 s)
essential_bound_scal..................proved - incomplete [shostak](0.40 s)
essential_bound_add...................proved - incomplete [shostak](0.27 s)
essential_bound_opp...................proved - incomplete [shostak](0.22 s)
essential_bound_diff..................proved - incomplete [shostak](1.09 s)
essential_bound_eq_0..................proved - incomplete [shostak](0.18 s)
essential_bound_prod..................proved - incomplete [shostak](0.30 s)
holder_judge_infty_1..................proved - incomplete [shostak](0.32 s)
holder_judge_infty_2..................proved - incomplete [shostak](0.70 s)
holder_infty_1........................proved - incomplete [shostak](0.36 s)
holder_infty_2........................proved - incomplete [shostak](0.22 s)
Theory totals: 21 formulas, 21 attempted, 21 succeeded (7.86 s)
Proof summary for theory essential_bound_complete_scaf
mu_TCC1...............................proved - complete [shostak](0.04 s)
essential_bound_complete_scaf.........proved - incomplete [shostak](5.07 s)
Theory totals: 2 formulas, 2 attempted, 2 succeeded (5.11 s)
Proof summary for theory cal_L_inf
mu_TCC1...............................proved - complete [shostak](0.04 s)
cal_L_infty_TCC1......................proved - complete [shostak](0.13 s)
cal_L_infty_is_essentially_bounded....proved - complete [shostak](0.46 s)
scal_cal_L_infty......................proved - incomplete [shostak](0.07 s)
add_cal_L_infty.......................proved - incomplete [shostak](0.07 s)
opp_cal_L_infty.......................proved - incomplete [shostak](0.07 s)
diff_cal_L_infty......................proved - incomplete [shostak](0.07 s)
prod_cal_L_infty......................proved - incomplete [shostak](0.07 s)
inf_norm_scal.........................proved - incomplete [shostak](0.40 s)
inf_norm_add..........................proved - incomplete [shostak](0.28 s)
inf_norm_opp..........................proved - incomplete [shostak](0.07 s)
inf_norm_diff.........................proved - incomplete [shostak](0.08 s)
inf_norm_eq_0.........................proved - incomplete [shostak](0.51 s)
inf_norm_prod.........................proved - incomplete [shostak](0.29 s)
holder_infty_1........................proved - incomplete [shostak](0.07 s)
Theory totals: 15 formulas, 15 attempted, 15 succeeded (2.69 s)
Proof summary for theory complex_finite_measures
mu_TCC1...............................proved - complete [shostak](0.04 s)
q_integrable_is_p_integrable..........proved - incomplete [shostak](0.81 s)
essentially_bounded_is_p_integrable...proved - incomplete [shostak](0.32 s)
Theory totals: 3 formulas, 3 attempted, 3 succeeded (1.16 s)
Proof summary for theory cal_L_complex
mu_TCC1...............................proved - complete [shostak](0.05 s)
cal_L_complex_infty_TCC1..............proved - complete [shostak](0.17 s)
cal_L_complex_infty_TCC2..............proved - complete [shostak](0.10 s)
cal_L_complex_infty_is_essentially_bounded...proved - complete [shostak](0.05 s)
cal_L_complex_TCC1....................proved - incomplete [shostak](0.12 s)
cal_L_complex_TCC2....................proved - incomplete [shostak](0.12 s)
cal_L_complex_is_p_integrable.........proved - complete [shostak](0.05 s)
cal_L_complex_1_def...................proved - incomplete [shostak](0.45 s)
scal_cal_L............................proved - incomplete [shostak](0.06 s)
sum_cal_L.............................proved - incomplete [shostak](0.05 s)
opp_cal_L.............................proved - incomplete [shostak](0.05 s)
diff_cal_L............................proved - incomplete [shostak](0.06 s)
prod_cal_L_TCC1.......................proved - complete [shostak](0.04 s)
prod_cal_L_TCC2.......................proved - complete [shostak](0.05 s)
prod_cal_L............................proved - incomplete [shostak](0.14 s)
scal_cal_L_infty......................proved - incomplete [shostak](0.06 s)
sum_cal_L_infty.......................proved - incomplete [shostak](0.06 s)
opp_cal_L_infty.......................proved - incomplete [shostak](0.06 s)
diff_cal_L_infty......................proved - incomplete [shostak](0.05 s)
prod_cal_L_infty......................proved - incomplete [shostak](0.06 s)
prod_cal_L_1_infty....................proved - incomplete [shostak](0.05 s)
prod_cal_L_infty_1....................proved - incomplete [shostak](0.06 s)
scal_cal_L_fm.........................proved - incomplete [shostak](0.05 s)
sum_cal_L_fm..........................proved - incomplete [shostak](0.06 s)
opp_cal_L_fm..........................proved - incomplete [shostak](0.05 s)
diff_cal_L_fm.........................proved - incomplete [shostak](0.05 s)
prod_cal_L_fm.........................proved - incomplete [shostak](0.11 s)
scal_cal_L_infty_fm...................proved - incomplete [shostak](0.05 s)
sum_cal_L_infty_fm....................proved - incomplete [shostak](0.06 s)
opp_cal_L_infty_fm....................proved - incomplete [shostak](0.05 s)
diff_cal_L_infty_fm...................proved - incomplete [shostak](0.05 s)
prod_cal_L_infty_fm...................proved - incomplete [shostak](0.05 s)
prod_cal_L_1_infty_fm.................proved - incomplete [shostak](0.05 s)
prod_cal_L_infty_1_fm.................proved - incomplete [shostak](0.05 s)
Theory totals: 34 formulas, 34 attempted, 34 succeeded (2.65 s)
Proof summary for theory cal_L_real
mu_TCC1...............................proved - complete [shostak](0.05 s)
cal_L_real_infty_TCC1.................proved - complete [shostak](0.15 s)
cal_L_real_infty_TCC2.................proved - complete [shostak](0.17 s)
cal_L_real_TCC1.......................proved - incomplete [shostak](0.09 s)
cal_L_real_TCC2.......................proved - incomplete [shostak](0.10 s)
cal_L_real_1_def......................proved - incomplete [shostak](0.07 s)
scal_cal_LR...........................proved - incomplete [shostak](0.08 s)
sum_cal_LR............................proved - incomplete [shostak](0.07 s)
opp_cal_LR............................proved - incomplete [shostak](0.05 s)
diff_cal_LR...........................proved - incomplete [shostak](0.07 s)
prod_cal_LR_TCC1......................proved - complete [shostak](0.04 s)
prod_cal_LR_TCC2......................proved - complete [shostak](0.05 s)
prod_cal_LR...........................proved - incomplete [shostak](0.14 s)
scal_cal_L_inftyR.....................proved - incomplete [shostak](0.11 s)
sum_cal_L_inftyR......................proved - incomplete [shostak](0.06 s)
opp_cal_L_inftyR......................proved - incomplete [shostak](0.06 s)
diff_cal_L_inftyR.....................proved - incomplete [shostak](0.06 s)
prod_cal_L_inftyR.....................proved - incomplete [shostak](0.12 s)
prod_cal_L_1_inftyR...................proved - incomplete [shostak](0.11 s)
prod_cal_L_infty_1R...................proved - incomplete [shostak](0.11 s)
scal_cal_L_fmR........................proved - incomplete [shostak](0.06 s)
sum_cal_L_fmR.........................proved - incomplete [shostak](0.05 s)
opp_cal_L_fmR.........................proved - incomplete [shostak](0.05 s)
diff_cal_L_fmR........................proved - incomplete [shostak](0.04 s)
prod_cal_L_fmR........................proved - incomplete [shostak](0.12 s)
scal_cal_L_infty_fmR..................proved - incomplete [shostak](0.05 s)
sum_cal_L_infty_fmR...................proved - incomplete [shostak](0.05 s)
opp_cal_L_infty_fmR...................proved - incomplete [shostak](0.05 s)
diff_cal_L_infty_fmR..................proved - incomplete [shostak](0.05 s)
prod_cal_L_infty_fmR..................proved - incomplete [shostak](0.05 s)
prod_cal_L_1_infty_fmR................proved - incomplete [shostak](0.06 s)
prod_cal_L_infty_1_fmR................proved - incomplete [shostak](0.06 s)
Theory totals: 32 formulas, 32 attempted, 32 succeeded (2.45 s)
Grand Totals: 179 proofs, 179 attempted, 179 succeeded (46.91 s)
[ Dauer der Verarbeitung: 0.106 Sekunden
]
|
|
