Structure integrationTheory
signature integrationTheory =
sig
type thm = Thm.thm
(* Definitions *)
val FINE : thm
val absolutely_integrable_on : thm
val division_of : thm
val division_points : thm
val equiintegrable_on : thm
val gauge_def : thm
val has_bounded_setvariation_on : thm
val has_bounded_variation_on : thm
val has_integral_compact_interval : thm
val has_integral_def : thm
val integrable_on : thm
val integral_def : thm
val negligible : thm
val operative : thm
val set_variation : thm
val tagged_division_of : thm
val tagged_partial_division_of : thm
val vector_variation : thm
(* Theorems *)
val ABSOLUTELY_INTEGRABLE_0 : thm
val ABSOLUTELY_INTEGRABLE_ABS : thm
val ABSOLUTELY_INTEGRABLE_ABSOLUTELY_INTEGRABLE_BOUND : thm
val ABSOLUTELY_INTEGRABLE_ABSOLUTELY_INTEGRABLE_COMPONENT_LBOUND : thm
val ABSOLUTELY_INTEGRABLE_ABSOLUTELY_INTEGRABLE_COMPONENT_UBOUND : thm
val ABSOLUTELY_INTEGRABLE_ABSOLUTELY_INTEGRABLE_LBOUND : thm
val ABSOLUTELY_INTEGRABLE_ABSOLUTELY_INTEGRABLE_UBOUND : thm
val ABSOLUTELY_INTEGRABLE_ABS_EQ : thm
val ABSOLUTELY_INTEGRABLE_ADD : thm
val ABSOLUTELY_INTEGRABLE_BOUNDED_SETVARIATION : thm
val ABSOLUTELY_INTEGRABLE_BOUNDED_SETVARIATION_EQ : thm
val ABSOLUTELY_INTEGRABLE_BOUNDED_SETVARIATION_UNIV_EQ : thm
val ABSOLUTELY_INTEGRABLE_CMUL : thm
val ABSOLUTELY_INTEGRABLE_COMPONENTWISE : thm
val ABSOLUTELY_INTEGRABLE_CONST : thm
val ABSOLUTELY_INTEGRABLE_CONTINUOUS : thm
val ABSOLUTELY_INTEGRABLE_EQ : thm
val ABSOLUTELY_INTEGRABLE_IMP_ABS_INTEGRABLE : thm
val ABSOLUTELY_INTEGRABLE_IMP_INTEGRABLE : thm
val ABSOLUTELY_INTEGRABLE_INF : thm
val ABSOLUTELY_INTEGRABLE_INTEGRABLE_BOUND : thm
val ABSOLUTELY_INTEGRABLE_LE : thm
val ABSOLUTELY_INTEGRABLE_LINEAR : thm
val ABSOLUTELY_INTEGRABLE_MAX : thm
val ABSOLUTELY_INTEGRABLE_MIN : thm
val ABSOLUTELY_INTEGRABLE_NEG : thm
val ABSOLUTELY_INTEGRABLE_ON_NULL : thm
val ABSOLUTELY_INTEGRABLE_ON_SUBINTERVAL : thm
val ABSOLUTELY_INTEGRABLE_RESTRICT_INTER : thm
val ABSOLUTELY_INTEGRABLE_RESTRICT_UNIV : thm
val ABSOLUTELY_INTEGRABLE_SET_VARIATION : thm
val ABSOLUTELY_INTEGRABLE_SPIKE : thm
val ABSOLUTELY_INTEGRABLE_SUB : thm
val ABSOLUTELY_INTEGRABLE_SUM : thm
val ABSOLUTELY_INTEGRABLE_SUP : thm
val ADDITIVE_CONTENT_DIVISION : thm
val ADDITIVE_CONTENT_TAGGED_DIVISION : thm
val ADDITIVE_TAGGED_DIVISION_1 : thm
val ANTIDERIVATIVE_CONTINUOUS : thm
val ANTIDERIVATIVE_INTEGRAL_CONTINUOUS : thm
val APPROXIMABLE_ON_DIVISION : thm
val BEPPO_LEVI_DECREASING : thm
val BEPPO_LEVI_INCREASING : thm
val BEPPO_LEVI_MONOTONE_CONVERGENCE_DECREASING : thm
val BEPPO_LEVI_MONOTONE_CONVERGENCE_DECREASING_AE : thm
val BEPPO_LEVI_MONOTONE_CONVERGENCE_INCREASING : thm
val BEPPO_LEVI_MONOTONE_CONVERGENCE_INCREASING_AE : thm
val BOUNDED_EQUIINTEGRAL_OVER_THIN_TAGGED_PARTIAL_DIVISION : thm
val BOUNDED_SETVARIATION_ABSOLUTELY_INTEGRABLE : thm
val BOUNDED_SETVARIATION_ABSOLUTELY_INTEGRABLE_INTERVAL : thm
val CONTENT_DOUBLESPLIT : thm
val CONTENT_IMAGE_AFFINITY_INTERVAL : thm
val CONTENT_IMAGE_STRETCH_INTERVAL : thm
val CONTENT_SPLIT : thm
val CONTINUOUS_ON_VECTOR_VARIATION : thm
val CONVEX_CONTAINS_SEGMENT : thm
val DECREASING_BOUNDED_VARIATION : thm
val DECREASING_BOUNDED_VARIATION_GEN : thm
val DECREASING_LEFT_LIMIT : thm
val DECREASING_RIGHT_LIMIT : thm
val DECREASING_VECTOR_VARIATION : thm
val DIVISION_1_SORT : thm
val DIVISION_COMMON_POINT_BOUND : thm
val DIVISION_CONTAINS : thm
val DIVISION_DISJOINT_UNION : thm
val DIVISION_DOUBLESPLIT : thm
val DIVISION_INTER : thm
val DIVISION_INTER_1 : thm
val DIVISION_OF : thm
val DIVISION_OF_AFFINITY : thm
val DIVISION_OF_BIGUNION : thm
val DIVISION_OF_CLOSED : thm
val DIVISION_OF_CONTENT_0 : thm
val DIVISION_OF_FINITE : thm
val DIVISION_OF_NONTRIVIAL : thm
val DIVISION_OF_REFLECT : thm
val DIVISION_OF_SELF : thm
val DIVISION_OF_SING : thm
val DIVISION_OF_SUBSET : thm
val DIVISION_OF_TAGGED_DIVISION : thm
val DIVISION_OF_TRANSLATION : thm
val DIVISION_OF_TRIVIAL : thm
val DIVISION_OF_UNION_SELF : thm
val DIVISION_POINTS_FINITE : thm
val DIVISION_POINTS_PSUBSET : thm
val DIVISION_POINTS_SUBSET : thm
val DIVISION_SPLIT : thm
val DIVISION_SPLIT_LEFT_INJ : thm
val DIVISION_SPLIT_LEFT_RIGHT_INJ : thm
val DIVISION_SPLIT_RIGHT_INJ : thm
val DIVISION_UNION_INTERVALS_EXISTS : thm
val DOMINATED_CONVERGENCE : thm
val DOMINATED_CONVERGENCE_ABSOLUTELY_INTEGRABLE : thm
val DOMINATED_CONVERGENCE_AE : thm
val DOMINATED_CONVERGENCE_INTEGRABLE : thm
val DSUM_BOUND : thm
val ELEMENTARY_BIGINTER : thm
val ELEMENTARY_BIGUNION_INTERVALS : thm
val ELEMENTARY_BOUNDED : thm
val ELEMENTARY_COMPACT : thm
val ELEMENTARY_EMPTY : thm
val ELEMENTARY_INTER : thm
val ELEMENTARY_INTERVAL : thm
val ELEMENTARY_SUBSET_INTERVAL : thm
val ELEMENTARY_UNION : thm
val ELEMENTARY_UNION_INTERVAL : thm
val ELEMENTARY_UNION_INTERVAL_STRONG : thm
val EMPTY_DIVISION_OF : thm
val EQUIINTEGRABLE_ADD : thm
val EQUIINTEGRABLE_CLOSED_INTERVAL_RESTRICTIONS : thm
val EQUIINTEGRABLE_CMUL : thm
val EQUIINTEGRABLE_DIVISION : thm
val EQUIINTEGRABLE_EQ : thm
val EQUIINTEGRABLE_HALFSPACE_RESTRICTIONS_GE : thm
val EQUIINTEGRABLE_HALFSPACE_RESTRICTIONS_GT : thm
val EQUIINTEGRABLE_HALFSPACE_RESTRICTIONS_LE : thm
val EQUIINTEGRABLE_HALFSPACE_RESTRICTIONS_LT : thm
val EQUIINTEGRABLE_LIMIT : thm
val EQUIINTEGRABLE_NEG : thm
val EQUIINTEGRABLE_ON_NULL : thm
val EQUIINTEGRABLE_ON_SING : thm
val EQUIINTEGRABLE_ON_SPLIT : thm
val EQUIINTEGRABLE_OPEN_INTERVAL_RESTRICTIONS : thm
val EQUIINTEGRABLE_REFLECT : thm
val EQUIINTEGRABLE_SUB : thm
val EQUIINTEGRABLE_SUBSET : thm
val EQUIINTEGRABLE_SUM : thm
val EQUIINTEGRABLE_UNIFORM_LIMIT : thm
val EQUIINTEGRABLE_UNION : thm
val FATOU : thm
val FINE_BIGINTER : thm
val FINE_BIGUNION : thm
val FINE_DIVISION_EXISTS : thm
val FINE_INTER : thm
val FINE_SUBSET : thm
val FINE_UNION : thm
val FINITE_POWERSET : thm
val FLOOR_POS : thm
val FORALL_IN_DIVISION : thm
val FORALL_IN_DIVISION_NONEMPTY : thm
val FUNDAMENTAL_THEOREM_OF_CALCULUS : thm
val FUNDAMENTAL_THEOREM_OF_CALCULUS_INTERIOR : thm
val FUNDAMENTAL_THEOREM_OF_CALCULUS_INTERIOR_STRONG : thm
val FUNDAMENTAL_THEOREM_OF_CALCULUS_STRONG : thm
val GAUGE_BALL : thm
val GAUGE_BALL_DEPENDENT : thm
val GAUGE_BIGINTER : thm
val GAUGE_EXISTENCE_LEMMA : thm
val GAUGE_INTER : thm
val GAUGE_MODIFY : thm
val GAUGE_TRIVIAL : thm
val HAS_BOUNDED_SETVARIATION_COMPARISON : thm
val HAS_BOUNDED_SETVARIATION_ON : thm
val HAS_BOUNDED_SETVARIATION_ON_0 : thm
val HAS_BOUNDED_SETVARIATION_ON_ABS : thm
val HAS_BOUNDED_SETVARIATION_ON_ADD : thm
val HAS_BOUNDED_SETVARIATION_ON_CMUL : thm
val HAS_BOUNDED_SETVARIATION_ON_COMPONENTWISE : thm
val HAS_BOUNDED_SETVARIATION_ON_COMPOSE_LINEAR : thm
val HAS_BOUNDED_SETVARIATION_ON_DIVISION : thm
val HAS_BOUNDED_SETVARIATION_ON_ELEMENTARY : thm
val HAS_BOUNDED_SETVARIATION_ON_EQ : thm
val HAS_BOUNDED_SETVARIATION_ON_IMP_BOUNDED_ON_SUBINTERVALS : thm
val HAS_BOUNDED_SETVARIATION_ON_INTERVAL : thm
val HAS_BOUNDED_SETVARIATION_ON_NEG : thm
val HAS_BOUNDED_SETVARIATION_ON_NULL : thm
val HAS_BOUNDED_SETVARIATION_ON_SUB : thm
val HAS_BOUNDED_SETVARIATION_ON_SUBSET : thm
val HAS_BOUNDED_SETVARIATION_ON_SUM : thm
val HAS_BOUNDED_SETVARIATION_ON_SUM_AND_SET_VARIATION_SUM_LE : thm
val HAS_BOUNDED_SETVARIATION_ON_UNIV : thm
val HAS_BOUNDED_SETVARIATION_REFLECT2_EQ : thm
val HAS_BOUNDED_SETVARIATION_REFLECT2_EQ_AND_SET_VARIATION_REFLECT2 : thm
val HAS_BOUNDED_SETVARIATION_TRANSLATION : thm
val HAS_BOUNDED_SETVARIATION_TRANSLATION2_EQ : thm
val HAS_BOUNDED_SETVARIATION_TRANSLATION2_EQ_AND_SET_VARIATION_TRANSLATION2 : thm
val HAS_BOUNDED_SETVARIATION_WORKS : thm
val HAS_BOUNDED_SETVARIATION_WORKS_ON_ELEMENTARY : thm
val HAS_BOUNDED_SETVARIATION_WORKS_ON_INTERVAL : thm
val HAS_BOUNDED_VARIATION_AFFINITY2_EQ : thm
val HAS_BOUNDED_VARIATION_AFFINITY2_EQ_AND_VECTOR_VARIATION_AFFINITY2 : thm
val HAS_BOUNDED_VARIATION_AFFINITY_EQ : thm
val HAS_BOUNDED_VARIATION_AFFINITY_EQ_AND_VECTOR_VARIATION_AFFINITY : thm
val HAS_BOUNDED_VARIATION_COMPARISON : thm
val HAS_BOUNDED_VARIATION_COMPOSE_DECREASING : thm
val HAS_BOUNDED_VARIATION_COMPOSE_INCREASING : thm
val HAS_BOUNDED_VARIATION_DARBOUX : thm
val HAS_BOUNDED_VARIATION_DARBOUX_STRICT : thm
val HAS_BOUNDED_VARIATION_DARBOUX_STRONG : thm
val HAS_BOUNDED_VARIATION_NONTRIVIAL : thm
val HAS_BOUNDED_VARIATION_ON_ABS : thm
val HAS_BOUNDED_VARIATION_ON_ADD : thm
val HAS_BOUNDED_VARIATION_ON_CLOSURE : thm
val HAS_BOUNDED_VARIATION_ON_CMUL : thm
val HAS_BOUNDED_VARIATION_ON_COMBINE : thm
val HAS_BOUNDED_VARIATION_ON_COMBINE_GEN : thm
val HAS_BOUNDED_VARIATION_ON_COMPONENTWISE : thm
val HAS_BOUNDED_VARIATION_ON_COMPOSE_LINEAR : thm
val HAS_BOUNDED_VARIATION_ON_CONST : thm
val HAS_BOUNDED_VARIATION_ON_DIVISION : thm
val HAS_BOUNDED_VARIATION_ON_EMPTY : thm
val HAS_BOUNDED_VARIATION_ON_EQ : thm
val HAS_BOUNDED_VARIATION_ON_ID : thm
val HAS_BOUNDED_VARIATION_ON_IMP_BOUNDED : thm
val HAS_BOUNDED_VARIATION_ON_IMP_BOUNDED_ON_INTERVAL : thm
val HAS_BOUNDED_VARIATION_ON_IMP_BOUNDED_ON_SUBINTERVALS : thm
val HAS_BOUNDED_VARIATION_ON_INDEFINITE_INTEGRAL_LEFT : thm
val HAS_BOUNDED_VARIATION_ON_INDEFINITE_INTEGRAL_RIGHT : thm
val HAS_BOUNDED_VARIATION_ON_MAX : thm
val HAS_BOUNDED_VARIATION_ON_MIN : thm
val HAS_BOUNDED_VARIATION_ON_MUL : thm
val HAS_BOUNDED_VARIATION_ON_NEG : thm
val HAS_BOUNDED_VARIATION_ON_NULL : thm
val HAS_BOUNDED_VARIATION_ON_REFLECT : thm
val HAS_BOUNDED_VARIATION_ON_REFLECT_INTERVAL : thm
val HAS_BOUNDED_VARIATION_ON_SING : thm
val HAS_BOUNDED_VARIATION_ON_SUB : thm
val HAS_BOUNDED_VARIATION_ON_SUBSET : thm
val HAS_BOUNDED_VARIATION_ON_SUM : thm
val HAS_BOUNDED_VARIATION_ON_SUM_AND_SUM_LE : thm
val HAS_BOUNDED_VARIATION_REFLECT2_EQ : thm
val HAS_BOUNDED_VARIATION_REFLECT2_EQ_AND_VECTOR_VARIATION_REFLECT2 : thm
val HAS_BOUNDED_VARIATION_REFLECT_EQ : thm
val HAS_BOUNDED_VARIATION_REFLECT_EQ_AND_VECTOR_VARIATION_REFLECT : thm
val HAS_BOUNDED_VARIATION_REFLECT_EQ_INTERVAL : thm
val HAS_BOUNDED_VARIATION_REFLECT_EQ_INTERVAL_AND_VECTOR_VARIATION_REFLECT_INTERVAL : thm
val HAS_BOUNDED_VARIATION_SUM_LE : thm
val HAS_BOUNDED_VARIATION_TRANSLATION : thm
val HAS_BOUNDED_VARIATION_TRANSLATION2_EQ : thm
val HAS_BOUNDED_VARIATION_TRANSLATION2_EQ_AND_VECTOR_VARIATION_TRANSLATION2 : thm
val HAS_BOUNDED_VARIATION_TRANSLATION_EQ : thm
val HAS_BOUNDED_VARIATION_TRANSLATION_EQ_AND_VECTOR_VARIATION_TRANSLATION : thm
val HAS_BOUNDED_VARIATION_TRANSLATION_EQ_INTERVAL : thm
val HAS_BOUNDED_VARIATION_TRANSLATION_EQ_INTERVAL_AND_VECTOR_VARIATION_TRANSLATION_INTERVAL : thm
val HAS_BOUNDED_VECTOR_VARIATION_LEFT_LIMIT : thm
val HAS_BOUNDED_VECTOR_VARIATION_RIGHT_LIMIT : thm
val HAS_DERIVATIVE_ZERO_UNIQUE_STRONG_INTERVAL : thm
val HAS_INTEGRAL : thm
val HAS_INTEGRAL_0 : thm
val HAS_INTEGRAL_0_EQ : thm
val HAS_INTEGRAL_ABS_BOUND_INTEGRAL_COMPONENT : thm
val HAS_INTEGRAL_ADD : thm
val HAS_INTEGRAL_AFFINITY : thm
val HAS_INTEGRAL_ALT : thm
val HAS_INTEGRAL_BIGUNION : thm
val HAS_INTEGRAL_BOUND : thm
val HAS_INTEGRAL_CLOSURE : thm
val HAS_INTEGRAL_CMUL : thm
val HAS_INTEGRAL_COMBINE : thm
val HAS_INTEGRAL_COMBINE_DIVISION : thm
val HAS_INTEGRAL_COMBINE_DIVISION_TOPDOWN : thm
val HAS_INTEGRAL_COMBINE_TAGGED_DIVISION : thm
val HAS_INTEGRAL_COMBINE_TAGGED_DIVISION_TOPDOWN : thm
val HAS_INTEGRAL_COMPONENTWISE : thm
val HAS_INTEGRAL_COMPONENT_LBOUND : thm
val HAS_INTEGRAL_COMPONENT_LE : thm
val HAS_INTEGRAL_COMPONENT_LE_AE : thm
val HAS_INTEGRAL_COMPONENT_NEG : thm
val HAS_INTEGRAL_COMPONENT_POS : thm
val HAS_INTEGRAL_COMPONENT_UBOUND : thm
val HAS_INTEGRAL_CONST : thm
val HAS_INTEGRAL_DIFF : thm
val HAS_INTEGRAL_DROP_LE : thm
val HAS_INTEGRAL_DROP_NEG : thm
val HAS_INTEGRAL_DROP_POS : thm
val HAS_INTEGRAL_DROP_POS_AE : thm
val HAS_INTEGRAL_EMPTY : thm
val HAS_INTEGRAL_EMPTY_EQ : thm
val HAS_INTEGRAL_EQ : thm
val HAS_INTEGRAL_EQ_EQ : thm
val HAS_INTEGRAL_FACTOR_CONTENT : thm
val HAS_INTEGRAL_INTEGRABLE : thm
val HAS_INTEGRAL_INTEGRABLE_INTEGRAL : thm
val HAS_INTEGRAL_INTEGRAL : thm
val HAS_INTEGRAL_INTERIOR : thm
val HAS_INTEGRAL_IS_0 : thm
val HAS_INTEGRAL_LE_AE : thm
val HAS_INTEGRAL_LIM_AT_POSINFINITY : thm
val HAS_INTEGRAL_LIM_SEQUENTIALLY : thm
val HAS_INTEGRAL_LINEAR : thm
val HAS_INTEGRAL_NEG : thm
val HAS_INTEGRAL_NEGLIGIBLE : thm
val HAS_INTEGRAL_NEGLIGIBLE_EQ : thm
val HAS_INTEGRAL_NULL : thm
val HAS_INTEGRAL_NULL_EQ : thm
val HAS_INTEGRAL_ON_SUPERSET : thm
val HAS_INTEGRAL_REFL : thm
val HAS_INTEGRAL_REFLECT : thm
val HAS_INTEGRAL_REFLECT_GEN : thm
val HAS_INTEGRAL_REFLECT_LEMMA : thm
val HAS_INTEGRAL_RESTRICT : thm
val HAS_INTEGRAL_RESTRICT_CLOSED_SUBINTERVAL : thm
val HAS_INTEGRAL_RESTRICT_CLOSED_SUBINTERVALS_EQ : thm
val HAS_INTEGRAL_RESTRICT_INTER : thm
val HAS_INTEGRAL_RESTRICT_OPEN_SUBINTERVAL : thm
val HAS_INTEGRAL_RESTRICT_UNIV : thm
val HAS_INTEGRAL_SEPARATE_SIDES : thm
val HAS_INTEGRAL_SPIKE : thm
val HAS_INTEGRAL_SPIKE_EQ : thm
val HAS_INTEGRAL_SPIKE_FINITE : thm
val HAS_INTEGRAL_SPIKE_FINITE_EQ : thm
val HAS_INTEGRAL_SPIKE_INTERIOR : thm
val HAS_INTEGRAL_SPIKE_INTERIOR_EQ : thm
val HAS_INTEGRAL_SPIKE_SET : thm
val HAS_INTEGRAL_SPIKE_SET_EQ : thm
val HAS_INTEGRAL_SPLIT : thm
val HAS_INTEGRAL_STRADDLE_NULL : thm
val HAS_INTEGRAL_STRETCH : thm
val HAS_INTEGRAL_SUB : thm
val HAS_INTEGRAL_SUBSET_COMPONENT_LE : thm
val HAS_INTEGRAL_SUBSET_DROP_LE : thm
val HAS_INTEGRAL_SUM : thm
val HAS_INTEGRAL_TWIDDLE : thm
val HAS_INTEGRAL_UNION : thm
val HAS_INTEGRAL_UNIQUE : thm
val HENSTOCK_LEMMA : thm
val HENSTOCK_LEMMA_PART1 : thm
val HENSTOCK_LEMMA_PART2 : thm
val INCREASING_BOUNDED_VARIATION : thm
val INCREASING_BOUNDED_VARIATION_GEN : thm
val INCREASING_LEFT_LIMIT : thm
val INCREASING_RIGHT_LIMIT : thm
val INCREASING_VECTOR_VARIATION : thm
val INDEFINITE_INTEGRAL_CONTINUOUS : thm
val INDEFINITE_INTEGRAL_CONTINUOUS_LEFT : thm
val INDEFINITE_INTEGRAL_CONTINUOUS_RIGHT : thm
val INTEGRABLE_0 : thm
val INTEGRABLE_ADD : thm
val INTEGRABLE_AFFINITY : thm
val INTEGRABLE_ALT : thm
val INTEGRABLE_ALT_SUBSET : thm
val INTEGRABLE_BOUNDED_VARIATION : thm
val INTEGRABLE_BOUNDED_VARIATION_BILINEAR_LMUL : thm
val INTEGRABLE_BOUNDED_VARIATION_BILINEAR_RMUL : thm
val INTEGRABLE_BOUNDED_VARIATION_PRODUCT : thm
val INTEGRABLE_BOUNDED_VARIATION_PRODUCT_ALT : thm
val INTEGRABLE_BY_PARTS : thm
val INTEGRABLE_BY_PARTS_EQ : thm
val INTEGRABLE_CASES : thm
val INTEGRABLE_CAUCHY : thm
val INTEGRABLE_CMUL : thm
val INTEGRABLE_CMUL_EQ : thm
val INTEGRABLE_COMBINE : thm
val INTEGRABLE_COMBINE_DIVISION : thm
val INTEGRABLE_COMPONENTWISE : thm
val INTEGRABLE_CONST : thm
val INTEGRABLE_CONTINUOUS : thm
val INTEGRABLE_DECREASING : thm
val INTEGRABLE_DECREASING_PRODUCT : thm
val INTEGRABLE_DECREASING_PRODUCT_UNIV : thm
val INTEGRABLE_EQ : thm
val INTEGRABLE_INCREASING : thm
val INTEGRABLE_INCREASING_PRODUCT : thm
val INTEGRABLE_INCREASING_PRODUCT_UNIV : thm
val INTEGRABLE_INTEGRAL : thm
val INTEGRABLE_LINEAR : thm
val INTEGRABLE_MIN_CONST : thm
val INTEGRABLE_NEG : thm
val INTEGRABLE_ON_ALL_INTERVALS_INTEGRABLE_BOUND : thm
val INTEGRABLE_ON_EMPTY : thm
val INTEGRABLE_ON_LITTLE_SUBINTERVALS : thm
val INTEGRABLE_ON_NULL : thm
val INTEGRABLE_ON_REFL : thm
val INTEGRABLE_ON_SUBDIVISION : thm
val INTEGRABLE_ON_SUBINTERVAL : thm
val INTEGRABLE_ON_SUPERSET : thm
val INTEGRABLE_REFLECT : thm
val INTEGRABLE_REFLECT_GEN : thm
val INTEGRABLE_RESTRICT : thm
val INTEGRABLE_RESTRICT_INTER : thm
val INTEGRABLE_RESTRICT_UNIV : thm
val INTEGRABLE_SPIKE : thm
val INTEGRABLE_SPIKE_EQ : thm
val INTEGRABLE_SPIKE_FINITE : thm
val INTEGRABLE_SPIKE_INTERIOR : thm
val INTEGRABLE_SPIKE_SET : thm
val INTEGRABLE_SPIKE_SET_EQ : thm
val INTEGRABLE_SPLIT : thm
val INTEGRABLE_STRADDLE : thm
val INTEGRABLE_STRADDLE_INTERVAL : thm
val INTEGRABLE_STRETCH : thm
val INTEGRABLE_SUB : thm
val INTEGRABLE_SUBINTERVAL : thm
val INTEGRABLE_SUM : thm
val INTEGRABLE_UNIFORM_LIMIT : thm
val INTEGRAL_0 : thm
val INTEGRAL_ABS_BOUND_INTEGRAL : thm
val INTEGRAL_ABS_BOUND_INTEGRAL_AE : thm
val INTEGRAL_ABS_BOUND_INTEGRAL_COMPONENT : thm
val INTEGRAL_ADD : thm
val INTEGRAL_CMUL : thm
val INTEGRAL_COMBINE : thm
val INTEGRAL_COMBINE_DIVISION_BOTTOMUP : thm
val INTEGRAL_COMBINE_DIVISION_TOPDOWN : thm
val INTEGRAL_COMBINE_TAGGED_DIVISION_BOTTOMUP : thm
val INTEGRAL_COMBINE_TAGGED_DIVISION_TOPDOWN : thm
val INTEGRAL_COMPONENT : thm
val INTEGRAL_COMPONENT_LBOUND : thm
val INTEGRAL_COMPONENT_LE : thm
val INTEGRAL_COMPONENT_LE_AE : thm
val INTEGRAL_COMPONENT_POS : thm
val INTEGRAL_COMPONENT_UBOUND : thm
val INTEGRAL_CONST : thm
val INTEGRAL_DIFF : thm
val INTEGRAL_DROP_LE : thm
val INTEGRAL_DROP_POS : thm
val INTEGRAL_DROP_POS_AE : thm
val INTEGRAL_EMPTY : thm
val INTEGRAL_EQ : thm
val INTEGRAL_EQ_0 : thm
val INTEGRAL_EQ_HAS_INTEGRAL : thm
val INTEGRAL_HAS_VECTOR_DERIVATIVE : thm
val INTEGRAL_HAS_VECTOR_DERIVATIVE_POINTWISE : thm
val INTEGRAL_LE_AE : thm
val INTEGRAL_LINEAR : thm
val INTEGRAL_NEG : thm
val INTEGRAL_NULL : thm
val INTEGRAL_REFL : thm
val INTEGRAL_REFLECT : thm
val INTEGRAL_REFLECT_GEN : thm
val INTEGRAL_RESTRICT : thm
val INTEGRAL_RESTRICT_INTER : thm
val INTEGRAL_RESTRICT_UNIV : thm
val INTEGRAL_SPIKE : thm
val INTEGRAL_SPIKE_SET : thm
val INTEGRAL_SPLIT : thm
val INTEGRAL_SPLIT_SIGNED : thm
val INTEGRAL_SUB : thm
val INTEGRAL_SUBSET_COMPONENT_LE : thm
val INTEGRAL_SUBSET_DROP_LE : thm
val INTEGRAL_SUM : thm
val INTEGRAL_UNION : thm
val INTEGRAL_UNIQUE : thm
val INTEGRATION_BY_PARTS : thm
val INTEGRATION_BY_PARTS_SIMPLE : thm
val INTERIOR_SUBSET_UNION_INTERVALS : thm
val INTERVAL_BISECTION : thm
val INTERVAL_BISECTION_STEP : thm
val INTERVAL_DOUBLESPLIT : thm
val INTERVAL_IMAGE_AFFINITY_INTERVAL : thm
val INTERVAL_SPLIT : thm
val INTERVAL_SUBDIVISION : thm
val INTER_INTERIOR_BIGUNION_INTERVALS : thm
val MONOTONE_CONVERGENCE_DECREASING : thm
val MONOTONE_CONVERGENCE_DECREASING_AE : thm
val MONOTONE_CONVERGENCE_INCREASING : thm
val MONOTONE_CONVERGENCE_INCREASING_AE : thm
val MONOTONE_CONVERGENCE_INTERVAL : thm
val NEGLIGIBLE : thm
val NEGLIGIBLE_BIGUNION : thm
val NEGLIGIBLE_BOUNDED_SUBSETS : thm
val NEGLIGIBLE_COUNTABLE : thm
val NEGLIGIBLE_COUNTABLE_BIGUNION : thm
val NEGLIGIBLE_DIFF : thm
val NEGLIGIBLE_EMPTY : thm
val NEGLIGIBLE_FINITE : thm
val NEGLIGIBLE_FRONTIER_INTERVAL : thm
val NEGLIGIBLE_INSERT : thm
val NEGLIGIBLE_INTER : thm
val NEGLIGIBLE_ON_COUNTABLE_INTERVALS : thm
val NEGLIGIBLE_ON_INTERVALS : thm
val NEGLIGIBLE_ON_UNIV : thm
val NEGLIGIBLE_SING : thm
val NEGLIGIBLE_STANDARD_HYPERPLANE : thm
val NEGLIGIBLE_SUBSET : thm
val NEGLIGIBLE_UNION : thm
val NEGLIGIBLE_UNION_EQ : thm
val NONNEGATIVE_ABSOLUTELY_INTEGRABLE : thm
val NONNEGATIVE_ABSOLUTELY_INTEGRABLE_AE : thm
val OPERATIVE_1_LE : thm
val OPERATIVE_1_LT : thm
val OPERATIVE_APPROXIMABLE : thm
val OPERATIVE_CONTENT : thm
val OPERATIVE_DIVISION : thm
val OPERATIVE_DIVISION_AND : thm
val OPERATIVE_EMPTY : thm
val OPERATIVE_FUNCTION_ENDPOINT_DIFF : thm
val OPERATIVE_INTEGRABLE : thm
val OPERATIVE_INTEGRAL : thm
val OPERATIVE_LIFTED_SETVARIATION : thm
val OPERATIVE_LIFTED_VECTOR_VARIATION : thm
val OPERATIVE_REAL_FUNCTION_ENDPOINT_DIFF : thm
val OPERATIVE_TAGGED_DIVISION : thm
val OPERATIVE_TRIVIAL : thm
val PARTIAL_DIVISION_EXTEND : thm
val PARTIAL_DIVISION_EXTEND_1 : thm
val PARTIAL_DIVISION_EXTEND_INTERVAL : thm
val PARTIAL_DIVISION_OF_TAGGED_DIVISION : thm
val PROPERTY_EMPTY_INTERVAL : thm
val REAL_MUL_POS_LT : thm
val RSUM_BOUND : thm
val RSUM_COMPONENT_LE : thm
val RSUM_DIFF_BOUND : thm
val SECOND_MEAN_VALUE_THEOREM : thm
val SECOND_MEAN_VALUE_THEOREM_BONNET : thm
val SECOND_MEAN_VALUE_THEOREM_BONNET_FULL : thm
val SECOND_MEAN_VALUE_THEOREM_FULL : thm
val SECOND_MEAN_VALUE_THEOREM_GEN : thm
val SECOND_MEAN_VALUE_THEOREM_GEN_FULL : thm
val SETVARIATION_EQUAL_LEMMA : thm
val SET_VARIATION : thm
val SET_VARIATION_0 : thm
val SET_VARIATION_COMPARISON : thm
val SET_VARIATION_ELEMENTARY_LEMMA : thm
val SET_VARIATION_EQ : thm
val SET_VARIATION_GE_FUNCTION : thm
val SET_VARIATION_LBOUND : thm
val SET_VARIATION_LBOUND_ON_INTERVAL : thm
val SET_VARIATION_MONOTONE : thm
val SET_VARIATION_ON_DIVISION : thm
val SET_VARIATION_ON_ELEMENTARY : thm
val SET_VARIATION_ON_INTERVAL : thm
val SET_VARIATION_ON_NULL : thm
val SET_VARIATION_POS_LE : thm
val SET_VARIATION_REFLECT2 : thm
val SET_VARIATION_SUM_LE : thm
val SET_VARIATION_TRANSLATION2 : thm
val SET_VARIATION_TRIANGLE : thm
val SET_VARIATION_UBOUND : thm
val SET_VARIATION_UBOUND_ON_INTERVAL : thm
val SET_VARIATION_WORKS_ON_INTERVAL : thm
val SUBADDITIVE_CONTENT_DIVISION : thm
val SUM_ABS_ALLSUBSETS_BOUND : thm
val SUM_CONTENT_AREA_OVER_THIN_DIVISION : thm
val SUM_CONTENT_NULL : thm
val SUM_NONZERO_IMAGE_LEMMA : thm
val SUM_OVER_TAGGED_DIVISION_LEMMA : thm
val SUM_OVER_TAGGED_PARTIAL_DIVISION_LEMMA : thm
val TAGGED_DIVISION_BIGUNION : thm
val TAGGED_DIVISION_BIGUNION_EXISTS : thm
val TAGGED_DIVISION_FINER : thm
val TAGGED_DIVISION_OF : thm
val TAGGED_DIVISION_OF_ALT : thm
val TAGGED_DIVISION_OF_ANOTHER : thm
val TAGGED_DIVISION_OF_EMPTY : thm
val TAGGED_DIVISION_OF_FINITE : thm
val TAGGED_DIVISION_OF_NONTRIVIAL : thm
val TAGGED_DIVISION_OF_SELF : thm
val TAGGED_DIVISION_OF_TRIVIAL : thm
val TAGGED_DIVISION_OF_UNION_SELF : thm
val TAGGED_DIVISION_SPLIT_LEFT_INJ : thm
val TAGGED_DIVISION_SPLIT_RIGHT_INJ : thm
val TAGGED_DIVISION_UNION : thm
val TAGGED_DIVISION_UNION_IMAGE_SND : thm
val TAGGED_DIVISION_UNION_INTERVAL : thm
val TAGGED_PARTIAL_DIVISION_COMMON_POINT_BOUND : thm
val TAGGED_PARTIAL_DIVISION_COMMON_TAGS : thm
val TAGGED_PARTIAL_DIVISION_OF_SUBSET : thm
val TAGGED_PARTIAL_DIVISION_OF_TRIVIAL : thm
val TAGGED_PARTIAL_DIVISION_OF_UNION_SELF : thm
val TAGGED_PARTIAL_DIVISION_SUBSET : thm
val TAG_IN_INTERVAL : thm
val VARIATION_EQUAL_LEMMA : thm
val VECTOR_VARIATION_ABS : thm
val VECTOR_VARIATION_AFFINITY : thm
val VECTOR_VARIATION_AFFINITY2 : thm
val VECTOR_VARIATION_COMBINE : thm
val VECTOR_VARIATION_COMPARISON : thm
val VECTOR_VARIATION_CONST : thm
val VECTOR_VARIATION_CONST_EQ : thm
val VECTOR_VARIATION_CONTINUOUS : thm
val VECTOR_VARIATION_CONTINUOUS_LEFT : thm
val VECTOR_VARIATION_CONTINUOUS_RIGHT : thm
val VECTOR_VARIATION_EQ : thm
val VECTOR_VARIATION_GE_ABS_FUNCTION : thm
val VECTOR_VARIATION_GE_FUNCTION : thm
val VECTOR_VARIATION_MINUS_FUNCTION_MONOTONE : thm
val VECTOR_VARIATION_MONOTONE : thm
val VECTOR_VARIATION_NEG : thm
val VECTOR_VARIATION_ON_DIVISION : thm
val VECTOR_VARIATION_ON_NULL : thm
val VECTOR_VARIATION_POS_LE : thm
val VECTOR_VARIATION_REFLECT : thm
val VECTOR_VARIATION_REFLECT2 : thm
val VECTOR_VARIATION_REFLECT_INTERVAL : thm
val VECTOR_VARIATION_TRANSLATION : thm
val VECTOR_VARIATION_TRANSLATION2 : thm
val VECTOR_VARIATION_TRANSLATION_INTERVAL : thm
val VECTOR_VARIATION_TRIANGLE : thm
val has_integral : thm
val has_integral_alt : thm
val integration_grammars : type_grammar.grammar * term_grammar.grammar
(*
[derivative] Parent theory of "integration"
[FINE] Definition
⊢ ∀d s. d FINE s ⇔ ∀x k. (x,k) ∈ s ⇒ k ⊆ d x
[absolutely_integrable_on] Definition
⊢ ∀f s.
f absolutely_integrable_on s ⇔
f integrable_on s ∧ (λx. abs (f x)) integrable_on s
[division_of] Definition
⊢ ∀s i.
s division_of i ⇔
FINITE s ∧
(∀k. k ∈ s ⇒ k ⊆ i ∧ k ≠ ∅ ∧ ∃a b. k = interval [(a,b)]) ∧
(∀k1 k2.
k1 ∈ s ∧ k2 ∈ s ∧ k1 ≠ k2 ⇒ interior k1 ∩ interior k2 = ∅) ∧
BIGUNION s = i
[division_points] Definition
⊢ ∀k d.
division_points k d =
{(j,x) |
1 ≤ j ∧ j ≤ 1 ∧ interval_lowerbound k < x ∧
x < interval_upperbound k ∧
∃i. i ∈ d ∧
(interval_lowerbound i = x ∨ interval_upperbound i = x)}
[equiintegrable_on] Definition
⊢ ∀fs i.
fs equiintegrable_on i ⇔
(∀f. f ∈ fs ⇒ f integrable_on i) ∧
∀e. 0 < e ⇒
∃d. gauge d ∧
∀f p.
f ∈ fs ∧ p tagged_division_of i ∧ d FINE p ⇒
abs (sum p (λ(x,k). content k * f x) − integral i f) <
e
[gauge_def] Definition
⊢ ∀d. gauge d ⇔ ∀x. x ∈ d x ∧ open (d x)
[has_bounded_setvariation_on] Definition
⊢ ∀f s.
f has_bounded_setvariation_on s ⇔
∃B. ∀d t. d division_of t ∧ t ⊆ s ⇒ sum d (λk. abs (f k)) ≤ B
[has_bounded_variation_on] Definition
⊢ ∀f s.
f has_bounded_variation_on s ⇔
(λk. f (interval_upperbound k) − f (interval_lowerbound k)) has_bounded_setvariation_on
s
[has_integral_compact_interval] Definition
⊢ ∀f y i.
(f has_integral_compact_interval y) i ⇔
∀e. 0 < e ⇒
∃d. gauge d ∧
∀p. p tagged_division_of i ∧ d FINE p ⇒
abs (sum p (λ(x,k). content k * f x) − y) < e
[has_integral_def] Definition
⊢ ∀f y i.
(f has_integral y) i ⇔
if ∃a b. i = interval [(a,b)] then
(f has_integral_compact_interval y) i
else
∀e. 0 < e ⇒
∃B. 0 < B ∧
∀a b.
ball (0,B) ⊆ interval [(a,b)] ⇒
∃z. ((λx. if x ∈ i then f x else 0) has_integral_compact_interval
z) (interval [(a,b)]) ∧ abs (z − y) < e
[integrable_on] Definition
⊢ ∀f i. f integrable_on i ⇔ ∃y. (f has_integral y) i
[integral_def] Definition
⊢ ∀i f. integral i f = @y. (f has_integral y) i
[negligible] Definition
⊢ ∀s. negligible s ⇔
∀a b. (indicator s has_integral 0) (interval [(a,b)])
[operative] Definition
⊢ ∀op f.
operative op f ⇔
(∀a b.
content (interval [(a,b)]) = 0 ⇒
f (interval [(a,b)]) = neutral op) ∧
∀a b c.
f (interval [(a,b)]) =
op (f (interval [(a,b)] ∩ {x | x ≤ c}))
(f (interval [(a,b)] ∩ {x | x ≥ c}))
[set_variation] Definition
⊢ ∀s f.
set_variation s f =
sup {sum d (λk. abs (f k)) | (∃t. d division_of t ∧ t ⊆ s)}
[tagged_division_of] Definition
⊢ ∀s i.
s tagged_division_of i ⇔
s tagged_partial_division_of i ∧
BIGUNION {k | (∃x. (x,k) ∈ s)} = i
[tagged_partial_division_of] Definition
⊢ ∀s i.
s tagged_partial_division_of i ⇔
FINITE s ∧
(∀x k. (x,k) ∈ s ⇒ x ∈ k ∧ k ⊆ i ∧ ∃a b. k = interval [(a,b)]) ∧
∀x1 k1 x2 k2.
(x1,k1) ∈ s ∧ (x2,k2) ∈ s ∧ (x1,k1) ≠ (x2,k2) ⇒
interior k1 ∩ interior k2 = ∅
[vector_variation] Definition
⊢ ∀s f.
vector_variation s f =
set_variation s
(λk. f (interval_upperbound k) − f (interval_lowerbound k))
[ABSOLUTELY_INTEGRABLE_0] Theorem
⊢ ∀s. (λx. 0) absolutely_integrable_on s
[ABSOLUTELY_INTEGRABLE_ABS] Theorem
⊢ ∀f s.
f absolutely_integrable_on s ⇒
(λx. abs (f x)) absolutely_integrable_on s
[ABSOLUTELY_INTEGRABLE_ABSOLUTELY_INTEGRABLE_BOUND] Theorem
⊢ ∀f g s.
(∀x. x ∈ s ⇒ abs (f x) ≤ abs (g x)) ∧ f integrable_on s ∧
g absolutely_integrable_on s ⇒
f absolutely_integrable_on s
[ABSOLUTELY_INTEGRABLE_ABSOLUTELY_INTEGRABLE_COMPONENT_LBOUND] Theorem
⊢ ∀f g s.
(∀x i. x ∈ s ⇒ f x ≤ g x) ∧ f absolutely_integrable_on s ∧
g integrable_on s ⇒
g absolutely_integrable_on s
[ABSOLUTELY_INTEGRABLE_ABSOLUTELY_INTEGRABLE_COMPONENT_UBOUND] Theorem
⊢ ∀f g s.
(∀x i. x ∈ s ⇒ f x ≤ g x) ∧ f integrable_on s ∧
g absolutely_integrable_on s ⇒
f absolutely_integrable_on s
[ABSOLUTELY_INTEGRABLE_ABSOLUTELY_INTEGRABLE_LBOUND] Theorem
⊢ ∀f g s.
(∀x. x ∈ s ⇒ f x ≤ g x) ∧ f absolutely_integrable_on s ∧
g integrable_on s ⇒
g absolutely_integrable_on s
[ABSOLUTELY_INTEGRABLE_ABSOLUTELY_INTEGRABLE_UBOUND] Theorem
⊢ ∀f g s.
(∀x. x ∈ s ⇒ f x ≤ g x) ∧ f integrable_on s ∧
g absolutely_integrable_on s ⇒
f absolutely_integrable_on s
[ABSOLUTELY_INTEGRABLE_ABS_EQ] Theorem
⊢ ∀f s.
f absolutely_integrable_on s ⇔
f integrable_on s ∧ (λx. abs (f x)) integrable_on s
[ABSOLUTELY_INTEGRABLE_ADD] Theorem
⊢ ∀f g s.
f absolutely_integrable_on s ∧ g absolutely_integrable_on s ⇒
(λx. f x + g x) absolutely_integrable_on s
[ABSOLUTELY_INTEGRABLE_BOUNDED_SETVARIATION] Theorem
⊢ ∀f s.
f absolutely_integrable_on s ⇒
(λk. integral k f) has_bounded_setvariation_on s
[ABSOLUTELY_INTEGRABLE_BOUNDED_SETVARIATION_EQ] Theorem
⊢ ∀f a b.
f absolutely_integrable_on interval [(a,b)] ⇔
f integrable_on interval [(a,b)] ∧
(λk. integral k f) has_bounded_setvariation_on interval [(a,b)]
[ABSOLUTELY_INTEGRABLE_BOUNDED_SETVARIATION_UNIV_EQ] Theorem
⊢ ∀f. f absolutely_integrable_on 𝕌(:real) ⇔
f integrable_on 𝕌(:real) ∧
(λk. integral k f) has_bounded_setvariation_on 𝕌(:real)
[ABSOLUTELY_INTEGRABLE_CMUL] Theorem
⊢ ∀f s c.
f absolutely_integrable_on s ⇒
(λx. c * f x) absolutely_integrable_on s
[ABSOLUTELY_INTEGRABLE_COMPONENTWISE] Theorem
⊢ ∀f s.
f absolutely_integrable_on s ⇔
(λx. f x) absolutely_integrable_on s
[ABSOLUTELY_INTEGRABLE_CONST] Theorem
⊢ ∀a b c. (λx. c) absolutely_integrable_on interval [(a,b)]
[ABSOLUTELY_INTEGRABLE_CONTINUOUS] Theorem
⊢ ∀f a b.
f continuous_on interval [(a,b)] ⇒
f absolutely_integrable_on interval [(a,b)]
[ABSOLUTELY_INTEGRABLE_EQ] Theorem
⊢ ∀f g s.
(∀x. x ∈ s ⇒ f x = g x) ∧ f absolutely_integrable_on s ⇒
g absolutely_integrable_on s
[ABSOLUTELY_INTEGRABLE_IMP_ABS_INTEGRABLE] Theorem
⊢ ∀f s.
f absolutely_integrable_on s ⇒ (λx. abs (f x)) integrable_on s
[ABSOLUTELY_INTEGRABLE_IMP_INTEGRABLE] Theorem
⊢ ∀f s. f absolutely_integrable_on s ⇒ f integrable_on s
[ABSOLUTELY_INTEGRABLE_INF] Theorem
⊢ ∀fs s k.
FINITE k ∧ k ≠ ∅ ∧
(∀i. i ∈ k ⇒ (λx. fs x i) absolutely_integrable_on s) ⇒
(λx. inf (IMAGE (fs x) k)) absolutely_integrable_on s
[ABSOLUTELY_INTEGRABLE_INTEGRABLE_BOUND] Theorem
⊢ ∀f g s.
(∀x. x ∈ s ⇒ abs (f x) ≤ g x) ∧ f integrable_on s ∧
g integrable_on s ⇒
f absolutely_integrable_on s
[ABSOLUTELY_INTEGRABLE_LE] Theorem
⊢ ∀f s.
f absolutely_integrable_on s ⇒
abs (integral s f) ≤ integral s (λx. abs (f x))
[ABSOLUTELY_INTEGRABLE_LINEAR] Theorem
⊢ ∀f h s.
f absolutely_integrable_on s ∧ linear h ⇒
h ∘ f absolutely_integrable_on s
[ABSOLUTELY_INTEGRABLE_MAX] Theorem
⊢ ∀f g s.
f absolutely_integrable_on s ∧ g absolutely_integrable_on s ⇒
(λx. max (f x) (g x)) absolutely_integrable_on s
[ABSOLUTELY_INTEGRABLE_MIN] Theorem
⊢ ∀f g s.
f absolutely_integrable_on s ∧ g absolutely_integrable_on s ⇒
(λx. min (f x) (g x)) absolutely_integrable_on s
[ABSOLUTELY_INTEGRABLE_NEG] Theorem
⊢ ∀f s.
f absolutely_integrable_on s ⇒
(λx. -f x) absolutely_integrable_on s
[ABSOLUTELY_INTEGRABLE_ON_NULL] Theorem
⊢ ∀f a b.
content (interval [(a,b)]) = 0 ⇒
f absolutely_integrable_on interval [(a,b)]
[ABSOLUTELY_INTEGRABLE_ON_SUBINTERVAL] Theorem
⊢ ∀f s a b.
f absolutely_integrable_on s ∧ interval [(a,b)] ⊆ s ⇒
f absolutely_integrable_on interval [(a,b)]
[ABSOLUTELY_INTEGRABLE_RESTRICT_INTER] Theorem
⊢ ∀f s t.
(λx. if x ∈ s then f x else 0) absolutely_integrable_on t ⇔
f absolutely_integrable_on s ∩ t
[ABSOLUTELY_INTEGRABLE_RESTRICT_UNIV] Theorem
⊢ ∀f s.
(λx. if x ∈ s then f x else 0) absolutely_integrable_on 𝕌(:real) ⇔
f absolutely_integrable_on s
[ABSOLUTELY_INTEGRABLE_SET_VARIATION] Theorem
⊢ ∀f a b.
f absolutely_integrable_on interval [(a,b)] ⇒
set_variation (interval [(a,b)]) (λk. integral k f) =
integral (interval [(a,b)]) (λx. abs (f x))
[ABSOLUTELY_INTEGRABLE_SPIKE] Theorem
⊢ ∀f g s t.
negligible s ∧ (∀x. x ∈ t DIFF s ⇒ g x = f x) ⇒
f absolutely_integrable_on t ⇒
g absolutely_integrable_on t
[ABSOLUTELY_INTEGRABLE_SUB] Theorem
⊢ ∀f g s.
f absolutely_integrable_on s ∧ g absolutely_integrable_on s ⇒
(λx. f x − g x) absolutely_integrable_on s
[ABSOLUTELY_INTEGRABLE_SUM] Theorem
⊢ ∀f s t.
FINITE t ∧ (∀a. a ∈ t ⇒ f a absolutely_integrable_on s) ⇒
(λx. sum t (λa. f a x)) absolutely_integrable_on s
[ABSOLUTELY_INTEGRABLE_SUP] Theorem
⊢ ∀fs s k.
FINITE k ∧ k ≠ ∅ ∧
(∀i. i ∈ k ⇒ (λx. fs x i) absolutely_integrable_on s) ⇒
(λx. sup (IMAGE (fs x) k)) absolutely_integrable_on s
[ADDITIVE_CONTENT_DIVISION] Theorem
⊢ ∀d a b.
d division_of interval [(a,b)] ⇒
sum d content = content (interval [(a,b)])
[ADDITIVE_CONTENT_TAGGED_DIVISION] Theorem
⊢ ∀d a b.
d tagged_division_of interval [(a,b)] ⇒
sum d (λ(x,l). content l) = content (interval [(a,b)])
[ADDITIVE_TAGGED_DIVISION_1] Theorem
⊢ ∀f p a b.
a ≤ b ∧ p tagged_division_of interval [(a,b)] ⇒
sum p
(λ(x,k). f (interval_upperbound k) − f (interval_lowerbound k)) =
f b − f a
[ANTIDERIVATIVE_CONTINUOUS] Theorem
⊢ ∀f a b.
f continuous_on interval [(a,b)] ⇒
∃g. ∀x.
x ∈ interval [(a,b)] ⇒
(g has_vector_derivative f x) (at x within interval [(a,b)])
[ANTIDERIVATIVE_INTEGRAL_CONTINUOUS] Theorem
⊢ ∀f a b.
f continuous_on interval [(a,b)] ⇒
∃g. ∀u v.
u ∈ interval [(a,b)] ∧ v ∈ interval [(a,b)] ∧ u ≤ v ⇒
(f has_integral g v − g u) (interval [(u,v)])
[APPROXIMABLE_ON_DIVISION] Theorem
⊢ ∀f d a b e.
0 ≤ e ∧ d division_of interval [(a,b)] ∧
(∀i. i ∈ d ⇒
∃g. (∀x. x ∈ i ⇒ abs (f x − g x) ≤ e) ∧ g integrable_on i) ⇒
∃g. (∀x. x ∈ interval [(a,b)] ⇒ abs (f x − g x) ≤ e) ∧
g integrable_on interval [(a,b)]
[BEPPO_LEVI_DECREASING] Theorem
⊢ ∀f s.
(∀k. f k integrable_on s) ∧ (∀k x. x ∈ s ⇒ f (SUC k) x ≤ f k x) ∧
bounded {integral s (f k) | k ∈ 𝕌(:num)} ⇒
∃g k.
negligible k ∧
∀x. x ∈ s DIFF k ⇒ ((λk. f k x) ⟶ g x) sequentially
[BEPPO_LEVI_INCREASING] Theorem
⊢ ∀f s.
(∀k. f k integrable_on s) ∧ (∀k x. x ∈ s ⇒ f k x ≤ f (SUC k) x) ∧
bounded {integral s (f k) | k ∈ 𝕌(:num)} ⇒
∃g k.
negligible k ∧
∀x. x ∈ s DIFF k ⇒ ((λk. f k x) ⟶ g x) sequentially
[BEPPO_LEVI_MONOTONE_CONVERGENCE_DECREASING] Theorem
⊢ ∀f s.
(∀k. f k integrable_on s) ∧ (∀k x. x ∈ s ⇒ f (SUC k) x ≤ f k x) ∧
bounded {integral s (f k) | k ∈ 𝕌(:num)} ⇒
∃g k.
negligible k ∧
(∀x. x ∈ s DIFF k ⇒ ((λk. f k x) ⟶ g x) sequentially) ∧
g integrable_on s ∧
((λk. integral s (f k)) ⟶ integral s g) sequentially
[BEPPO_LEVI_MONOTONE_CONVERGENCE_DECREASING_AE] Theorem
⊢ ∀f s.
(∀k. f k integrable_on s) ∧
(∀k. ∃t. negligible t ∧ ∀x. x ∈ s DIFF t ⇒ f (SUC k) x ≤ f k x) ∧
bounded {integral s (f k) | k ∈ 𝕌(:num)} ⇒
∃g k.
negligible k ∧
(∀x. x ∈ s DIFF k ⇒ ((λk. f k x) ⟶ g x) sequentially) ∧
g integrable_on s ∧
((λk. integral s (f k)) ⟶ integral s g) sequentially
[BEPPO_LEVI_MONOTONE_CONVERGENCE_INCREASING] Theorem
⊢ ∀f s.
(∀k. f k integrable_on s) ∧ (∀k x. x ∈ s ⇒ f k x ≤ f (SUC k) x) ∧
bounded {integral s (f k) | k ∈ 𝕌(:num)} ⇒
∃g k.
negligible k ∧
(∀x. x ∈ s DIFF k ⇒ ((λk. f k x) ⟶ g x) sequentially) ∧
g integrable_on s ∧
((λk. integral s (f k)) ⟶ integral s g) sequentially
[BEPPO_LEVI_MONOTONE_CONVERGENCE_INCREASING_AE] Theorem
⊢ ∀f s.
(∀k. f k integrable_on s) ∧
(∀k. ∃t. negligible t ∧ ∀x. x ∈ s DIFF t ⇒ f k x ≤ f (SUC k) x) ∧
bounded {integral s (f k) | k ∈ 𝕌(:num)} ⇒
∃g k.
negligible k ∧
(∀x. x ∈ s DIFF k ⇒ ((λk. f k x) ⟶ g x) sequentially) ∧
g integrable_on s ∧
((λk. integral s (f k)) ⟶ integral s g) sequentially
[BOUNDED_EQUIINTEGRAL_OVER_THIN_TAGGED_PARTIAL_DIVISION] Theorem
⊢ ∀fs f a b e.
fs equiintegrable_on interval [(a,b)] ∧ f ∈ fs ∧
(∀h x. h ∈ fs ∧ x ∈ interval [(a,b)] ⇒ abs (h x) ≤ abs (f x)) ∧
0 < e ⇒
∃d. gauge d ∧
∀c p h.
c ∈ interval [(a,b)] ∧
p tagged_partial_division_of interval [(a,b)] ∧ d FINE p ∧
h ∈ fs ∧ (∀x k. (x,k) ∈ p ⇒ k ∩ {x | x = c} ≠ ∅) ⇒
sum p (λ(x,k). abs (integral k h)) < e
[BOUNDED_SETVARIATION_ABSOLUTELY_INTEGRABLE] Theorem
⊢ ∀f. f integrable_on 𝕌(:real) ∧
(λk. integral k f) has_bounded_setvariation_on 𝕌(:real) ⇒
f absolutely_integrable_on 𝕌(:real)
[BOUNDED_SETVARIATION_ABSOLUTELY_INTEGRABLE_INTERVAL] Theorem
⊢ ∀f a b.
f integrable_on interval [(a,b)] ∧
(λk. integral k f) has_bounded_setvariation_on interval [(a,b)] ⇒
f absolutely_integrable_on interval [(a,b)]
[CONTENT_DOUBLESPLIT] Theorem
⊢ ∀a b c e.
0 < e ⇒
∃d. 0 < d ∧
content (interval [(a,b)] ∩ {x | abs (x − c) ≤ d}) < e
[CONTENT_IMAGE_AFFINITY_INTERVAL] Theorem
⊢ ∀a b m c.
content (IMAGE (λx. m * x + c) (interval [(a,b)])) =
abs m pow 1 * content (interval [(a,b)])
[CONTENT_IMAGE_STRETCH_INTERVAL] Theorem
⊢ ∀a b m.
content (IMAGE (λx. m 1 * x) (interval [(a,b)])) =
abs (product {1 .. 1} m) * content (interval [(a,b)])
[CONTENT_SPLIT] Theorem
⊢ ∀a b k.
content (interval [(a,b)]) =
content (interval [(a,b)] ∩ {x | x ≤ c}) +
content (interval [(a,b)] ∩ {x | x ≥ c})
[CONTINUOUS_ON_VECTOR_VARIATION] Theorem
⊢ ∀f a b.
f has_bounded_variation_on interval [(a,b)] ∧
f continuous_on interval [(a,b)] ⇒
(λx. vector_variation (interval [(a,x)]) f) continuous_on
interval [(a,b)]
[CONVEX_CONTAINS_SEGMENT] Theorem
⊢ ∀s. convex s ⇔ ∀a b. a ∈ s ∧ b ∈ s ⇒ segment [(a,b)] ⊆ s
[DECREASING_BOUNDED_VARIATION] Theorem
⊢ ∀f a b.
(∀x y.
x ∈ interval [(a,b)] ∧ y ∈ interval [(a,b)] ∧ x ≤ y ⇒
f y ≤ f x) ⇒
f has_bounded_variation_on interval [(a,b)]
[DECREASING_BOUNDED_VARIATION_GEN] Theorem
⊢ ∀f s.
bounded (IMAGE f s) ∧ (∀x y. x ∈ s ∧ y ∈ s ∧ x ≤ y ⇒ f y ≤ f x) ⇒
f has_bounded_variation_on s
[DECREASING_LEFT_LIMIT] Theorem
⊢ ∀f a b c.
(∀x y.
x ∈ interval [(a,b)] ∧ y ∈ interval [(a,b)] ∧ x ≤ y ⇒
f y ≤ f x) ∧ c ∈ interval [(a,b)] ⇒
∃l. (f ⟶ l) (at c within interval [(a,c)])
[DECREASING_RIGHT_LIMIT] Theorem
⊢ ∀f a b c.
(∀x y.
x ∈ interval [(a,b)] ∧ y ∈ interval [(a,b)] ∧ x ≤ y ⇒
f y ≤ f x) ∧ c ∈ interval [(a,b)] ⇒
∃l. (f ⟶ l) (at c within interval [(c,b)])
[DECREASING_VECTOR_VARIATION] Theorem
⊢ ∀f a b.
interval [(a,b)] ≠ ∅ ∧
(∀x y.
x ∈ interval [(a,b)] ∧ y ∈ interval [(a,b)] ∧ x ≤ y ⇒
f y ≤ f x) ⇒
vector_variation (interval [(a,b)]) f = f a − f b
[DIVISION_1_SORT] Theorem
⊢ ∀d s.
d division_of s ∧ (∀k. k ∈ d ⇒ interior k ≠ ∅) ⇒
∃n t.
IMAGE t {1 .. n} = d ∧
∀i j.
i ∈ {1 .. n} ∧ j ∈ {1 .. n} ∧ i < j ⇒
t i ≠ t j ∧ ∀x y. x ∈ t i ∧ y ∈ t j ⇒ x ≤ y
[DIVISION_COMMON_POINT_BOUND] Theorem
⊢ ∀d s x.
d division_of s ⇒
CARD {k | k ∈ d ∧ content k ≠ 0 ∧ x ∈ k} ≤ 2 ** 1
[DIVISION_CONTAINS] Theorem
⊢ ∀s i. s division_of i ⇒ ∀x. x ∈ i ⇒ ∃k. x ∈ k ∧ k ∈ s
[DIVISION_DISJOINT_UNION] Theorem
⊢ ∀s1 s2 p1 p2.
p1 division_of s1 ∧ p2 division_of s2 ∧
interior s1 ∩ interior s2 = ∅ ⇒
p1 ∪ p2 division_of s1 ∪ s2
[DIVISION_DOUBLESPLIT] Theorem
⊢ ∀p a b c e.
p division_of interval [(a,b)] ⇒
{l ∩ {x | abs (x − c) ≤ e} |
l |
l ∈ p ∧ l ∩ {x | abs (x − c) ≤ e} ≠ ∅} division_of
interval [(a,b)] ∩ {x | abs (x − c) ≤ e}
[DIVISION_INTER] Theorem
⊢ ∀s1 s2 p1 p2.
p1 division_of s1 ∧ p2 division_of s2 ⇒
{k1 ∩ k2 | k1 ∈ p1 ∧ k2 ∈ p2 ∧ k1 ∩ k2 ≠ ∅} division_of s1 ∩ s2
[DIVISION_INTER_1] Theorem
⊢ ∀d i a b.
d division_of i ∧ interval [(a,b)] ⊆ i ⇒
{interval [(a,b)] ∩ k | k | k ∈ d ∧ interval [(a,b)] ∩ k ≠ ∅} division_of
interval [(a,b)]
[DIVISION_OF] Theorem
⊢ ∀s i.
s division_of i ⇔
FINITE s ∧ (∀k. k ∈ s ⇒ k ≠ ∅ ∧ ∃a b. k = interval [(a,b)]) ∧
(∀k1 k2.
k1 ∈ s ∧ k2 ∈ s ∧ k1 ≠ k2 ⇒ interior k1 ∩ interior k2 = ∅) ∧
BIGUNION s = i
[DIVISION_OF_AFFINITY] Theorem
⊢ ∀d s m c.
IMAGE (IMAGE (λx. m * x + c)) d division_of
IMAGE (λx. m * x + c) s ⇔
if m = 0 then if s = ∅ then d = ∅ else d ≠ ∅ ∧ ∀k. k ∈ d ⇒ k ≠ ∅
else d division_of s
[DIVISION_OF_BIGUNION] Theorem
⊢ ∀f. FINITE f ∧ (∀p. p ∈ f ⇒ p division_of BIGUNION p) ∧
(∀k1 k2.
k1 ∈ BIGUNION f ∧ k2 ∈ BIGUNION f ∧ k1 ≠ k2 ⇒
interior k1 ∩ interior k2 = ∅) ⇒
BIGUNION f division_of BIGUNION (BIGUNION f)
[DIVISION_OF_CLOSED] Theorem
⊢ ∀s i. s division_of i ⇒ closed i
[DIVISION_OF_CONTENT_0] Theorem
⊢ ∀a b d.
content (interval [(a,b)]) = 0 ∧ d division_of interval [(a,b)] ⇒
∀k. k ∈ d ⇒ content k = 0
[DIVISION_OF_FINITE] Theorem
⊢ ∀s i. s division_of i ⇒ FINITE s
[DIVISION_OF_NONTRIVIAL] Theorem
⊢ ∀s a b.
s division_of interval [(a,b)] ∧ content (interval [(a,b)]) ≠ 0 ⇒
{k | k ∈ s ∧ content k ≠ 0} division_of interval [(a,b)]
[DIVISION_OF_REFLECT] Theorem
⊢ ∀d s.
IMAGE (IMAGE (λx. -x)) d division_of IMAGE (λx. -x) s ⇔
d division_of s
[DIVISION_OF_SELF] Theorem
⊢ ∀a b.
interval [(a,b)] ≠ ∅ ⇒
{interval [(a,b)]} division_of interval [(a,b)]
[DIVISION_OF_SING] Theorem
⊢ ∀s a. s division_of interval [(a,a)] ⇔ s = {interval [(a,a)]}
[DIVISION_OF_SUBSET] Theorem
⊢ ∀p q. p division_of BIGUNION p ∧ q ⊆ p ⇒ q division_of BIGUNION q
[DIVISION_OF_TAGGED_DIVISION] Theorem
⊢ ∀s i. s tagged_division_of i ⇒ IMAGE SND s division_of i
[DIVISION_OF_TRANSLATION] Theorem
⊢ ∀d s.
IMAGE (IMAGE (λx. a + x)) d division_of IMAGE (λx. a + x) s ⇔
d division_of s
[DIVISION_OF_TRIVIAL] Theorem
⊢ ∀s. s division_of ∅ ⇔ s = ∅
[DIVISION_OF_UNION_SELF] Theorem
⊢ ∀p s. p division_of s ⇒ p division_of BIGUNION p
[DIVISION_POINTS_FINITE] Theorem
⊢ ∀d i. d division_of i ⇒ FINITE (division_points i d)
[DIVISION_POINTS_PSUBSET] Theorem
⊢ ∀a b c d.
d division_of interval [(a,b)] ∧ a < b ∧ a < c ∧ c < b ∧
(∃l. l ∈ d ∧
(interval_lowerbound l = c ∨ interval_upperbound l = c)) ⇒
division_points (interval [(a,b)] ∩ {x | x ≤ c})
{l ∩ {x | x ≤ c} | l | l ∈ d ∧ l ∩ {x | x ≤ c} ≠ ∅} ⊂
division_points (interval [(a,b)]) d ∧
division_points (interval [(a,b)] ∩ {x | x ≥ c})
{l ∩ {x | x ≥ c} | l | l ∈ d ∧ l ∩ {x | x ≥ c} ≠ ∅} ⊂
division_points (interval [(a,b)]) d
[DIVISION_POINTS_SUBSET] Theorem
⊢ ∀a b c d k.
d division_of interval [(a,b)] ∧ a < b ∧ a < c ∧ c < b ⇒
division_points (interval [(a,b)] ∩ {x | x ≤ c})
{l ∩ {x | x ≤ c} | l | l ∈ d ∧ l ∩ {x | x ≤ c} ≠ ∅} ⊆
division_points (interval [(a,b)]) d ∧
division_points (interval [(a,b)] ∩ {x | x ≥ c})
{l ∩ {x | x ≥ c} | l | l ∈ d ∧ l ∩ {x | x ≥ c} ≠ ∅} ⊆
division_points (interval [(a,b)]) d
[DIVISION_SPLIT] Theorem
⊢ ∀p a b c.
p division_of interval [(a,b)] ⇒
{l ∩ {x | x ≤ c} | l | l ∈ p ∧ l ∩ {x | x ≤ c} ≠ ∅} division_of
interval [(a,b)] ∩ {x | x ≤ c} ∧
{l ∩ {x | x ≥ c} | l | l ∈ p ∧ l ∩ {x | x ≥ c} ≠ ∅} division_of
interval [(a,b)] ∩ {x | x ≥ c}
[DIVISION_SPLIT_LEFT_INJ] Theorem
⊢ ∀d i k1 k2 k c.
d division_of i ∧ k1 ∈ d ∧ k2 ∈ d ∧ k1 ≠ k2 ∧
k1 ∩ {x | x ≤ c} = k2 ∩ {x | x ≤ c} ⇒
content (k1 ∩ {x | x ≤ c}) = 0
[DIVISION_SPLIT_LEFT_RIGHT_INJ] Theorem
⊢ (∀d i k1 k2 k c.
d division_of i ∧ k1 ∈ d ∧ k2 ∈ d ∧ k1 ≠ k2 ∧
k1 ∩ {x | x ≤ c} = k2 ∩ {x | x ≤ c} ⇒
content (k1 ∩ {x | x ≤ c}) = 0) ∧
∀d i k1 k2 k c.
d division_of i ∧ k1 ∈ d ∧ k2 ∈ d ∧ k1 ≠ k2 ∧
k1 ∩ {x | x ≥ c} = k2 ∩ {x | x ≥ c} ⇒
content (k1 ∩ {x | x ≥ c}) = 0
[DIVISION_SPLIT_RIGHT_INJ] Theorem
⊢ ∀d i k1 k2 k c.
d division_of i ∧ k1 ∈ d ∧ k2 ∈ d ∧ k1 ≠ k2 ∧
k1 ∩ {x | x ≥ c} = k2 ∩ {x | x ≥ c} ⇒
content (k1 ∩ {x | x ≥ c}) = 0
[DIVISION_UNION_INTERVALS_EXISTS] Theorem
⊢ ∀a b c d.
interval [(a,b)] ≠ ∅ ⇒
∃p. interval [(a,b)] INSERT p division_of
interval [(a,b)] ∪ interval [(c,d)]
[DOMINATED_CONVERGENCE] Theorem
⊢ ∀f g h s.
(∀k. f k integrable_on s) ∧ h integrable_on s ∧
(∀k x. x ∈ s ⇒ abs (f k x) ≤ h x) ∧
(∀x. x ∈ s ⇒ ((λk. f k x) ⟶ g x) sequentially) ⇒
g integrable_on s ∧
((λk. integral s (f k)) ⟶ integral s g) sequentially
[DOMINATED_CONVERGENCE_ABSOLUTELY_INTEGRABLE] Theorem
⊢ ∀f g h s.
(∀k. f k absolutely_integrable_on s) ∧ h integrable_on s ∧
(∀k x. x ∈ s ⇒ abs (g x) ≤ h x) ∧
(∀x. x ∈ s ⇒ ((λk. f k x) ⟶ g x) sequentially) ⇒
g absolutely_integrable_on s
[DOMINATED_CONVERGENCE_AE] Theorem
⊢ ∀f g h s t.
(∀k. f k integrable_on s) ∧ h integrable_on s ∧ negligible t ∧
(∀k x. x ∈ s DIFF t ⇒ abs (f k x) ≤ h x) ∧
(∀x. x ∈ s DIFF t ⇒ ((λk. f k x) ⟶ g x) sequentially) ⇒
g integrable_on s ∧
((λk. integral s (f k)) ⟶ integral s g) sequentially
[DOMINATED_CONVERGENCE_INTEGRABLE] Theorem
⊢ ∀f g h s.
(∀k. f k absolutely_integrable_on s) ∧ h integrable_on s ∧
(∀k x. x ∈ s ⇒ abs (g x) ≤ h x) ∧
(∀x. x ∈ s ⇒ ((λk. f k x) ⟶ g x) sequentially) ⇒
g integrable_on s
[DSUM_BOUND] Theorem
⊢ ∀p a b c e.
p division_of interval [(a,b)] ∧ abs c ≤ e ⇒
abs (sum p (λl. content l * c)) ≤ e * content (interval [(a,b)])
[ELEMENTARY_BIGINTER] Theorem
⊢ ∀f. FINITE f ∧ f ≠ ∅ ∧ (∀s. s ∈ f ⇒ ∃p. p division_of s) ⇒
∃p. p division_of BIGINTER f
[ELEMENTARY_BIGUNION_INTERVALS] Theorem
⊢ ∀f. FINITE f ∧ (∀s. s ∈ f ⇒ ∃a b. s = interval [(a,b)]) ⇒
∃p. p division_of BIGUNION f
[ELEMENTARY_BOUNDED] Theorem
⊢ ∀s. (∃p. p division_of s) ⇒ bounded s
[ELEMENTARY_COMPACT] Theorem
⊢ ∀s. (∃d. d division_of s) ⇒ compact s
[ELEMENTARY_EMPTY] Theorem
⊢ ∃p. p division_of ∅
[ELEMENTARY_INTER] Theorem
⊢ ∀s t.
(∃p. p division_of s) ∧ (∃p. p division_of t) ⇒
∃p. p division_of s ∩ t
[ELEMENTARY_INTERVAL] Theorem
⊢ ∀a b. ∃p. p division_of interval [(a,b)]
[ELEMENTARY_SUBSET_INTERVAL] Theorem
⊢ ∀s. (∃p. p division_of s) ⇒ ∃a b. s ⊆ interval [(a,b)]
[ELEMENTARY_UNION] Theorem
⊢ ∀s t.
(∃p. p division_of s) ∧ (∃p. p division_of t) ⇒
∃p. p division_of s ∪ t
[ELEMENTARY_UNION_INTERVAL] Theorem
⊢ ∀p a b.
p division_of BIGUNION p ⇒
∃q. q division_of interval [(a,b)] ∪ BIGUNION p
[ELEMENTARY_UNION_INTERVAL_STRONG] Theorem
⊢ ∀p a b.
p division_of BIGUNION p ⇒
∃q. p ⊆ q ∧ q division_of interval [(a,b)] ∪ BIGUNION p
[EMPTY_DIVISION_OF] Theorem
⊢ ∀s. ∅ division_of s ⇔ s = ∅
[EQUIINTEGRABLE_ADD] Theorem
⊢ ∀fs gs s.
fs equiintegrable_on s ∧ gs equiintegrable_on s ⇒
{(λx. f x + g x) | f ∈ fs ∧ g ∈ gs} equiintegrable_on s
[EQUIINTEGRABLE_CLOSED_INTERVAL_RESTRICTIONS] Theorem
⊢ ∀f a b.
f integrable_on interval [(a,b)] ⇒
{(λx. if x ∈ interval [(c,d)] then f x else 0) |
c ∈ 𝕌(:real) ∧ d ∈ 𝕌(:real)} equiintegrable_on interval [(a,b)]
[EQUIINTEGRABLE_CMUL] Theorem
⊢ ∀fs s k.
fs equiintegrable_on s ⇒
{(λx. c * f x) | abs c ≤ k ∧ f ∈ fs} equiintegrable_on s
[EQUIINTEGRABLE_DIVISION] Theorem
⊢ ∀fs d a b.
d division_of interval [(a,b)] ⇒
(fs equiintegrable_on interval [(a,b)] ⇔
∀i. i ∈ d ⇒ fs equiintegrable_on i)
[EQUIINTEGRABLE_EQ] Theorem
⊢ ∀fs gs s.
fs equiintegrable_on s ∧
(∀g. g ∈ gs ⇒ ∃f. f ∈ fs ∧ ∀x. x ∈ s ⇒ f x = g x) ⇒
gs equiintegrable_on s
[EQUIINTEGRABLE_HALFSPACE_RESTRICTIONS_GE] Theorem
⊢ ∀fs f a b.
fs equiintegrable_on interval [(a,b)] ∧ f ∈ fs ∧
(∀h x. h ∈ fs ∧ x ∈ interval [(a,b)] ⇒ abs (h x) ≤ abs (f x)) ⇒
{(λx. if x ≥ c then h x else 0) | c ∈ 𝕌(:real) ∧ h ∈ fs} equiintegrable_on
interval [(a,b)]
[EQUIINTEGRABLE_HALFSPACE_RESTRICTIONS_GT] Theorem
⊢ ∀fs f a b.
fs equiintegrable_on interval [(a,b)] ∧ f ∈ fs ∧
(∀h x. h ∈ fs ∧ x ∈ interval [(a,b)] ⇒ abs (h x) ≤ abs (f x)) ⇒
{(λx. if x > c then h x else 0) | c ∈ 𝕌(:real) ∧ h ∈ fs} equiintegrable_on
interval [(a,b)]
[EQUIINTEGRABLE_HALFSPACE_RESTRICTIONS_LE] Theorem
⊢ ∀fs f a b.
fs equiintegrable_on interval [(a,b)] ∧ f ∈ fs ∧
(∀h x. h ∈ fs ∧ x ∈ interval [(a,b)] ⇒ abs (h x) ≤ abs (f x)) ⇒
{(λx. if x ≤ c then h x else 0) | c ∈ 𝕌(:real) ∧ h ∈ fs} equiintegrable_on
interval [(a,b)]
[EQUIINTEGRABLE_HALFSPACE_RESTRICTIONS_LT] Theorem
⊢ ∀fs f a b.
fs equiintegrable_on interval [(a,b)] ∧ f ∈ fs ∧
(∀h x. h ∈ fs ∧ x ∈ interval [(a,b)] ⇒ abs (h x) ≤ abs (f x)) ⇒
{(λx. if x < c then h x else 0) | c ∈ 𝕌(:real) ∧ h ∈ fs} equiintegrable_on
interval [(a,b)]
[EQUIINTEGRABLE_LIMIT] Theorem
⊢ ∀f g a b.
{f n | n ∈ 𝕌(:num)} equiintegrable_on interval [(a,b)] ∧
(∀x. x ∈ interval [(a,b)] ⇒ ((λn. f n x) ⟶ g x) sequentially) ⇒
g integrable_on interval [(a,b)] ∧
((λn. integral (interval [(a,b)]) (f n)) ⟶
integral (interval [(a,b)]) g) sequentially
[EQUIINTEGRABLE_NEG] Theorem
⊢ ∀fs s.
fs equiintegrable_on s ⇒
{(λx. -f x) | f ∈ fs} equiintegrable_on s
[EQUIINTEGRABLE_ON_NULL] Theorem
⊢ ∀fs a b.
content (interval [(a,b)]) = 0 ⇒
fs equiintegrable_on interval [(a,b)]
[EQUIINTEGRABLE_ON_SING] Theorem
⊢ ∀f a b.
{f} equiintegrable_on interval [(a,b)] ⇔
f integrable_on interval [(a,b)]
[EQUIINTEGRABLE_ON_SPLIT] Theorem
⊢ ∀fs k a b c.
fs equiintegrable_on interval [(a,b)] ∩ {x | x ≤ c} ∧
fs equiintegrable_on interval [(a,b)] ∩ {x | x ≥ c} ⇒
fs equiintegrable_on interval [(a,b)]
[EQUIINTEGRABLE_OPEN_INTERVAL_RESTRICTIONS] Theorem
⊢ ∀f a b.
f integrable_on interval [(a,b)] ⇒
{(λx. if x ∈ interval (c,d) then f x else 0) |
c ∈ 𝕌(:real) ∧ d ∈ 𝕌(:real)} equiintegrable_on interval [(a,b)]
[EQUIINTEGRABLE_REFLECT] Theorem
⊢ ∀fs a b.
fs equiintegrable_on interval [(a,b)] ⇒
{(λx. f (-x)) | f ∈ fs} equiintegrable_on interval [(-b,-a)]
[EQUIINTEGRABLE_SUB] Theorem
⊢ ∀fs gs s.
fs equiintegrable_on s ∧ gs equiintegrable_on s ⇒
{(λx. f x − g x) | f ∈ fs ∧ g ∈ gs} equiintegrable_on s
[EQUIINTEGRABLE_SUBSET] Theorem
⊢ ∀fs gs s. fs equiintegrable_on s ∧ gs ⊆ fs ⇒ gs equiintegrable_on s
[EQUIINTEGRABLE_SUM] Theorem
⊢ ∀fs a b.
fs equiintegrable_on interval [(a,b)] ⇒
{(λx. sum t (λi. c i * f i x)) |
FINITE t ∧ (∀i. i ∈ t ⇒ 0 ≤ c i ∧ f i ∈ fs) ∧ sum t c = 1} equiintegrable_on
interval [(a,b)]
[EQUIINTEGRABLE_UNIFORM_LIMIT] Theorem
⊢ ∀fs a b.
fs equiintegrable_on interval [(a,b)] ⇒
{g |
∀e. 0 < e ⇒
∃f. f ∈ fs ∧ ∀x. x ∈ interval [(a,b)] ⇒ abs (g x − f x) < e} equiintegrable_on
interval [(a,b)]
[EQUIINTEGRABLE_UNION] Theorem
⊢ ∀fs gs s.
fs equiintegrable_on s ∧ gs equiintegrable_on s ⇒
fs ∪ gs equiintegrable_on s
[FATOU] Theorem
⊢ ∀f g s t B.
negligible t ∧ (∀n. f n integrable_on s) ∧
(∀n x. x ∈ s DIFF t ⇒ 0 ≤ f n x) ∧
(∀x. x ∈ s DIFF t ⇒ ((λn. f n x) ⟶ g x) sequentially) ∧
(∀n. integral s (f n) ≤ B) ⇒
g integrable_on s ∧ 0 ≤ integral s g ∧ integral s g ≤ B
[FINE_BIGINTER] Theorem
⊢ ∀f s p.
(λx. BIGINTER {f d x | d ∈ s}) FINE p ⇔ ∀d. d ∈ s ⇒ f d FINE p
[FINE_BIGUNION] Theorem
⊢ ∀d ps. (∀p. p ∈ ps ⇒ d FINE p) ⇒ d FINE BIGUNION ps
[FINE_DIVISION_EXISTS] Theorem
⊢ ∀g a b.
gauge g ⇒ ∃p. p tagged_division_of interval [(a,b)] ∧ g FINE p
[FINE_INTER] Theorem
⊢ ∀p d1 d2. (λx. d1 x ∩ d2 x) FINE p ⇔ d1 FINE p ∧ d2 FINE p
[FINE_SUBSET] Theorem
⊢ ∀d p q. p ⊆ q ∧ d FINE q ⇒ d FINE p
[FINE_UNION] Theorem
⊢ ∀d p1 p2. d FINE p1 ∧ d FINE p2 ⇒ d FINE p1 ∪ p2
[FINITE_POWERSET] Theorem
⊢ ∀s. FINITE s ⇒ FINITE {t | t ⊆ s}
[FLOOR_POS] Theorem
⊢ ∀x. 0 ≤ x ⇒ ∃n. flr x = n
[FORALL_IN_DIVISION] Theorem
⊢ ∀P d i.
d division_of i ⇒
((∀x. x ∈ d ⇒ P x) ⇔
∀a b. interval [(a,b)] ∈ d ⇒ P (interval [(a,b)]))
[FORALL_IN_DIVISION_NONEMPTY] Theorem
⊢ ∀P d i.
d division_of i ⇒
((∀x. x ∈ d ⇒ P x) ⇔
∀a b.
interval [(a,b)] ∈ d ∧ interval [(a,b)] ≠ ∅ ⇒
P (interval [(a,b)]))
[FUNDAMENTAL_THEOREM_OF_CALCULUS] Theorem
⊢ ∀f f' a b.
a ≤ b ∧
(∀x. x ∈ interval [(a,b)] ⇒
(f has_vector_derivative f' x)
(at x within interval [(a,b)])) ⇒
(f' has_integral f b − f a) (interval [(a,b)])
[FUNDAMENTAL_THEOREM_OF_CALCULUS_INTERIOR] Theorem
⊢ ∀f f' a b.
a ≤ b ∧ f continuous_on interval [(a,b)] ∧
(∀x. x ∈ interval (a,b) ⇒ (f has_vector_derivative f' x) (at x)) ⇒
(f' has_integral f b − f a) (interval [(a,b)])
[FUNDAMENTAL_THEOREM_OF_CALCULUS_INTERIOR_STRONG] Theorem
⊢ ∀f f' s a b.
countable s ∧ a ≤ b ∧ f continuous_on interval [(a,b)] ∧
(∀x. x ∈ interval (a,b) DIFF s ⇒
(f has_vector_derivative f' x) (at x)) ⇒
(f' has_integral f b − f a) (interval [(a,b)])
[FUNDAMENTAL_THEOREM_OF_CALCULUS_STRONG] Theorem
⊢ ∀f f' s a b.
countable s ∧ a ≤ b ∧ f continuous_on interval [(a,b)] ∧
(∀x. x ∈ interval [(a,b)] DIFF s ⇒
(f has_vector_derivative f' x)
(at x within interval [(a,b)])) ⇒
(f' has_integral f b − f a) (interval [(a,b)])
[GAUGE_BALL] Theorem
⊢ ∀e. 0 < e ⇒ gauge (λx. ball (x,e))
[GAUGE_BALL_DEPENDENT] Theorem
⊢ ∀e. (∀x. 0 < e x) ⇒ gauge (λx. ball (x,e x))
[GAUGE_BIGINTER] Theorem
⊢ ∀f s.
FINITE s ∧ (∀d. d ∈ s ⇒ gauge (f d)) ⇒
gauge (λx. BIGINTER {f d x | d ∈ s})
[GAUGE_EXISTENCE_LEMMA] Theorem
⊢ ∀p q. (∀x. ∃d. p x ⇒ 0 < d ∧ q d x) ⇔ ∀x. ∃d. 0 < d ∧ (p x ⇒ q d x)
[GAUGE_INTER] Theorem
⊢ ∀d1 d2. gauge d1 ∧ gauge d2 ⇒ gauge (λx. d1 x ∩ d2 x)
[GAUGE_MODIFY] Theorem
⊢ ∀f. (∀s. open s ⇒ open {x | f x ∈ s}) ⇒
∀d. gauge d ⇒ gauge (λx y. d (f x) (f y))
[GAUGE_TRIVIAL] Theorem
⊢ gauge (λx. ball (x,1))
[HAS_BOUNDED_SETVARIATION_COMPARISON] Theorem
⊢ ∀f g s.
f has_bounded_setvariation_on s ∧
(∀a b.
interval [(a,b)] ≠ ∅ ∧ interval [(a,b)] ⊆ s ⇒
abs (g (interval [(a,b)])) ≤ abs (f (interval [(a,b)]))) ⇒
g has_bounded_setvariation_on s
[HAS_BOUNDED_SETVARIATION_ON] Theorem
⊢ ∀f s.
f has_bounded_setvariation_on s ⇔
∃B. 0 < B ∧
∀d t. d division_of t ∧ t ⊆ s ⇒ sum d (λk. abs (f k)) ≤ B
[HAS_BOUNDED_SETVARIATION_ON_0] Theorem
⊢ ∀s. (λx. 0) has_bounded_setvariation_on s
[HAS_BOUNDED_SETVARIATION_ON_ABS] Theorem
⊢ ∀f s.
(λx. abs (f x)) has_bounded_setvariation_on s ⇔
f has_bounded_setvariation_on s
[HAS_BOUNDED_SETVARIATION_ON_ADD] Theorem
⊢ ∀f g s.
f has_bounded_setvariation_on s ∧ g has_bounded_setvariation_on s ⇒
(λx. f x + g x) has_bounded_setvariation_on s
[HAS_BOUNDED_SETVARIATION_ON_CMUL] Theorem
⊢ ∀f c s.
f has_bounded_setvariation_on s ⇒
(λx. c * f x) has_bounded_setvariation_on s
[HAS_BOUNDED_SETVARIATION_ON_COMPONENTWISE] Theorem
⊢ ∀f s.
f has_bounded_setvariation_on s ⇔
(λk. f k) has_bounded_setvariation_on s
[HAS_BOUNDED_SETVARIATION_ON_COMPOSE_LINEAR] Theorem
⊢ ∀f g s.
f has_bounded_setvariation_on s ∧ linear g ⇒
g ∘ f has_bounded_setvariation_on s
[HAS_BOUNDED_SETVARIATION_ON_DIVISION] Theorem
⊢ ∀f a b d.
operative $+ f ∧ d division_of interval [(a,b)] ⇒
((∀k. k ∈ d ⇒ f has_bounded_setvariation_on k) ⇔
f has_bounded_setvariation_on interval [(a,b)])
[HAS_BOUNDED_SETVARIATION_ON_ELEMENTARY] Theorem
⊢ ∀f s.
(∃d. d division_of s) ⇒
(f has_bounded_setvariation_on s ⇔
∃B. ∀d. d division_of s ⇒ sum d (λk. abs (f k)) ≤ B)
[HAS_BOUNDED_SETVARIATION_ON_EQ] Theorem
⊢ ∀f g s.
(∀a b.
interval [(a,b)] ≠ ∅ ∧ interval [(a,b)] ⊆ s ⇒
f (interval [(a,b)]) = g (interval [(a,b)])) ∧
f has_bounded_setvariation_on s ⇒
g has_bounded_setvariation_on s
[HAS_BOUNDED_SETVARIATION_ON_IMP_BOUNDED_ON_SUBINTERVALS] Theorem
⊢ ∀f s.
f has_bounded_setvariation_on s ⇒
bounded {f (interval [(c,d)]) | interval [(c,d)] ⊆ s}
[HAS_BOUNDED_SETVARIATION_ON_INTERVAL] Theorem
⊢ ∀f a b.
f has_bounded_setvariation_on interval [(a,b)] ⇔
∃B. ∀d.
d division_of interval [(a,b)] ⇒ sum d (λk. abs (f k)) ≤ B
[HAS_BOUNDED_SETVARIATION_ON_NEG] Theorem
⊢ ∀f s.
(λx. -f x) has_bounded_setvariation_on s ⇔
f has_bounded_setvariation_on s
[HAS_BOUNDED_SETVARIATION_ON_NULL] Theorem
⊢ ∀f s.
(∀a b. content (interval [(a,b)]) = 0 ⇒ f (interval [(a,b)]) = 0) ∧
content s = 0 ∧ bounded s ⇒
f has_bounded_setvariation_on s
[HAS_BOUNDED_SETVARIATION_ON_SUB] Theorem
⊢ ∀f g s.
f has_bounded_setvariation_on s ∧ g has_bounded_setvariation_on s ⇒
(λx. f x − g x) has_bounded_setvariation_on s
[HAS_BOUNDED_SETVARIATION_ON_SUBSET] Theorem
⊢ ∀f s t.
f has_bounded_setvariation_on s ∧ t ⊆ s ⇒
f has_bounded_setvariation_on t
[HAS_BOUNDED_SETVARIATION_ON_SUM] Theorem
⊢ ∀f s k.
FINITE k ∧ (∀i. i ∈ k ⇒ f i has_bounded_setvariation_on s) ⇒
(λx. sum k (λi. f i x)) has_bounded_setvariation_on s
[HAS_BOUNDED_SETVARIATION_ON_SUM_AND_SET_VARIATION_SUM_LE] Theorem
⊢ (∀f s k.
FINITE k ∧ (∀i. i ∈ k ⇒ f i has_bounded_setvariation_on s) ⇒
(λx. sum k (λi. f i x)) has_bounded_setvariation_on s) ∧
∀f s k.
FINITE k ∧ (∀i. i ∈ k ⇒ f i has_bounded_setvariation_on s) ⇒
set_variation s (λx. sum k (λi. f i x)) ≤
sum k (λi. set_variation s (f i))
[HAS_BOUNDED_SETVARIATION_ON_UNIV] Theorem
⊢ ∀f. f has_bounded_setvariation_on 𝕌(:real) ⇔
∃B. ∀d. d division_of BIGUNION d ⇒ sum d (λk. abs (f k)) ≤ B
[HAS_BOUNDED_SETVARIATION_REFLECT2_EQ] Theorem
⊢ ∀f s.
(λk. f (IMAGE (λx. -x) k)) has_bounded_setvariation_on
IMAGE (λx. -x) s ⇔ f has_bounded_setvariation_on s
[HAS_BOUNDED_SETVARIATION_REFLECT2_EQ_AND_SET_VARIATION_REFLECT2] Theorem
⊢ (∀f s.
(λk. f (IMAGE (λx. -x) k)) has_bounded_setvariation_on
IMAGE (λx. -x) s ⇔ f has_bounded_setvariation_on s) ∧
∀f s.
set_variation (IMAGE (λx. -x) s) (λk. f (IMAGE (λx. -x) k)) =
set_variation s f
[HAS_BOUNDED_SETVARIATION_TRANSLATION] Theorem
⊢ ∀f s a.
f has_bounded_setvariation_on s ⇒
(λk. f (IMAGE (λx. a + x) k)) has_bounded_setvariation_on
IMAGE (λx. -a + x) s
[HAS_BOUNDED_SETVARIATION_TRANSLATION2_EQ] Theorem
⊢ ∀a f s.
(λk. f (IMAGE (λx. a + x) k)) has_bounded_setvariation_on
IMAGE (λx. -a + x) s ⇔ f has_bounded_setvariation_on s
[HAS_BOUNDED_SETVARIATION_TRANSLATION2_EQ_AND_SET_VARIATION_TRANSLATION2] Theorem
⊢ (∀a f s.
(λk. f (IMAGE (λx. a + x) k)) has_bounded_setvariation_on
IMAGE (λx. -a + x) s ⇔ f has_bounded_setvariation_on s) ∧
∀a f s.
set_variation (IMAGE (λx. -a + x) s)
(λk. f (IMAGE (λx. a + x) k)) =
set_variation s f
[HAS_BOUNDED_SETVARIATION_WORKS] Theorem
⊢ ∀f s.
f has_bounded_setvariation_on s ⇒
(∀d t.
d division_of t ∧ t ⊆ s ⇒
sum d (λk. abs (f k)) ≤ set_variation s f) ∧
∀B. (∀d t. d division_of t ∧ t ⊆ s ⇒ sum d (λk. abs (f k)) ≤ B) ⇒
set_variation s f ≤ B
[HAS_BOUNDED_SETVARIATION_WORKS_ON_ELEMENTARY] Theorem
⊢ ∀f s.
f has_bounded_setvariation_on s ∧ (∃d. d division_of s) ⇒
(∀d. d division_of s ⇒ sum d (λk. abs (f k)) ≤ set_variation s f) ∧
∀B. (∀d. d division_of s ⇒ sum d (λk. abs (f k)) ≤ B) ⇒
set_variation s f ≤ B
[HAS_BOUNDED_SETVARIATION_WORKS_ON_INTERVAL] Theorem
⊢ ∀f a b.
f has_bounded_setvariation_on interval [(a,b)] ⇒
(∀d. d division_of interval [(a,b)] ⇒
sum d (λk. abs (f k)) ≤ set_variation (interval [(a,b)]) f) ∧
∀B. (∀d. d division_of interval [(a,b)] ⇒
sum d (λk. abs (f k)) ≤ B) ⇒
set_variation (interval [(a,b)]) f ≤ B
[HAS_BOUNDED_VARIATION_AFFINITY2_EQ] Theorem
⊢ ∀m c f s.
(λx. f (m * x + c)) has_bounded_variation_on
IMAGE (λx. m⁻¹ * x + -(m⁻¹ * c)) s ⇔
m = 0 ∨ f has_bounded_variation_on s
[HAS_BOUNDED_VARIATION_AFFINITY2_EQ_AND_VECTOR_VARIATION_AFFINITY2] Theorem
⊢ (∀m c f s.
(λx. f (m * x + c)) has_bounded_variation_on
IMAGE (λx. m⁻¹ * x + -(m⁻¹ * c)) s ⇔
m = 0 ∨ f has_bounded_variation_on s) ∧
∀m c f s.
vector_variation (IMAGE (λx. m⁻¹ * x + -(m⁻¹ * c)) s)
(λx. f (m * x + c)) =
if m = 0 then 0 else vector_variation s f
[HAS_BOUNDED_VARIATION_AFFINITY_EQ] Theorem
⊢ ∀m c f s.
(λx. f (m * x + c)) has_bounded_variation_on s ⇔
m = 0 ∨ f has_bounded_variation_on IMAGE (λx. m * x + c) s
[HAS_BOUNDED_VARIATION_AFFINITY_EQ_AND_VECTOR_VARIATION_AFFINITY] Theorem
⊢ (∀m c f s.
(λx. f (m * x + c)) has_bounded_variation_on s ⇔
m = 0 ∨ f has_bounded_variation_on IMAGE (λx. m * x + c) s) ∧
∀m c f s.
vector_variation s (λx. f (m * x + c)) =
if m = 0 then 0 else vector_variation (IMAGE (λx. m * x + c) s) f
[HAS_BOUNDED_VARIATION_COMPARISON] Theorem
⊢ ∀f g s.
f has_bounded_variation_on s ∧
(∀x y. x ∈ s ∧ y ∈ s ∧ x < y ⇒ dist (g x,g y) ≤ dist (f x,f y)) ⇒
g has_bounded_variation_on s
[HAS_BOUNDED_VARIATION_COMPOSE_DECREASING] Theorem
⊢ ∀f g a b.
(∀x y.
x ∈ interval [(a,b)] ∧ y ∈ interval [(a,b)] ∧ x ≤ y ⇒
f y ≤ f x) ∧ g has_bounded_variation_on interval [(f b,f a)] ⇒
g ∘ f has_bounded_variation_on interval [(a,b)]
[HAS_BOUNDED_VARIATION_COMPOSE_INCREASING] Theorem
⊢ ∀f g a b.
(∀x y.
x ∈ interval [(a,b)] ∧ y ∈ interval [(a,b)] ∧ x ≤ y ⇒
f x ≤ f y) ∧ g has_bounded_variation_on interval [(f a,f b)] ⇒
g ∘ f has_bounded_variation_on interval [(a,b)]
[HAS_BOUNDED_VARIATION_DARBOUX] Theorem
⊢ ∀f a b.
f has_bounded_variation_on interval [(a,b)] ⇔
∃g h.
(∀x y.
x ∈ interval [(a,b)] ∧ y ∈ interval [(a,b)] ∧ x ≤ y ⇒
g x ≤ g y) ∧
(∀x y.
x ∈ interval [(a,b)] ∧ y ∈ interval [(a,b)] ∧ x ≤ y ⇒
h x ≤ h y) ∧ ∀x. f x = g x − h x
[HAS_BOUNDED_VARIATION_DARBOUX_STRICT] Theorem
⊢ ∀f a b.
f has_bounded_variation_on interval [(a,b)] ⇔
∃g h.
(∀x y.
x ∈ interval [(a,b)] ∧ y ∈ interval [(a,b)] ∧ x < y ⇒
g x < g y) ∧
(∀x y.
x ∈ interval [(a,b)] ∧ y ∈ interval [(a,b)] ∧ x < y ⇒
h x < h y) ∧ ∀x. f x = g x − h x
[HAS_BOUNDED_VARIATION_DARBOUX_STRONG] Theorem
⊢ ∀f a b.
f has_bounded_variation_on interval [(a,b)] ⇒
∃g h.
(∀x. f x = g x − h x) ∧
(∀x y.
x ∈ interval [(a,b)] ∧ y ∈ interval [(a,b)] ∧ x ≤ y ⇒
g x ≤ g y) ∧
(∀x y.
x ∈ interval [(a,b)] ∧ y ∈ interval [(a,b)] ∧ x ≤ y ⇒
h x ≤ h y) ∧
(∀x y.
x ∈ interval [(a,b)] ∧ y ∈ interval [(a,b)] ∧ x < y ⇒
g x < g y) ∧
(∀x y.
x ∈ interval [(a,b)] ∧ y ∈ interval [(a,b)] ∧ x < y ⇒
h x < h y) ∧
(∀x. x ∈ interval [(a,b)] ∧
f continuous (at x within interval [(a,x)]) ⇒
g continuous (at x within interval [(a,x)]) ∧
h continuous (at x within interval [(a,x)])) ∧
(∀x. x ∈ interval [(a,b)] ∧
f continuous (at x within interval [(x,b)]) ⇒
g continuous (at x within interval [(x,b)]) ∧
h continuous (at x within interval [(x,b)])) ∧
∀x. x ∈ interval [(a,b)] ∧
f continuous (at x within interval [(a,b)]) ⇒
g continuous (at x within interval [(a,b)]) ∧
h continuous (at x within interval [(a,b)])
[HAS_BOUNDED_VARIATION_NONTRIVIAL] Theorem
⊢ ∀f s.
f has_bounded_variation_on s ⇔
∃B. ∀d t.
d division_of t ∧ t ⊆ s ∧ (∀k. k ∈ d ⇒ interior k ≠ ∅) ⇒
sum d
(λk.
abs
(f (interval_upperbound k) − f (interval_lowerbound k))) ≤
B
[HAS_BOUNDED_VARIATION_ON_ABS] Theorem
⊢ ∀f s.
f has_bounded_variation_on s ⇒
(λx. abs (f x)) has_bounded_variation_on s
[HAS_BOUNDED_VARIATION_ON_ADD] Theorem
⊢ ∀f g s.
f has_bounded_variation_on s ∧ g has_bounded_variation_on s ⇒
(λx. f x + g x) has_bounded_variation_on s
[HAS_BOUNDED_VARIATION_ON_CLOSURE] Theorem
⊢ ∀f s.
is_interval s ∧ f has_bounded_variation_on s ⇒
f has_bounded_variation_on closure s
[HAS_BOUNDED_VARIATION_ON_CMUL] Theorem
⊢ ∀f c s.
f has_bounded_variation_on s ⇒
(λx. c * f x) has_bounded_variation_on s
[HAS_BOUNDED_VARIATION_ON_COMBINE] Theorem
⊢ ∀f a b c.
a ≤ c ∧ c ≤ b ⇒
(f has_bounded_variation_on interval [(a,b)] ⇔
f has_bounded_variation_on interval [(a,c)] ∧
f has_bounded_variation_on interval [(c,b)])
[HAS_BOUNDED_VARIATION_ON_COMBINE_GEN] Theorem
⊢ ∀f s a.
is_interval s ⇒
(f has_bounded_variation_on s ⇔
f has_bounded_variation_on {x | x ∈ s ∧ x ≤ a} ∧
f has_bounded_variation_on {x | x ∈ s ∧ x ≥ a})
[HAS_BOUNDED_VARIATION_ON_COMPONENTWISE] Theorem
⊢ ∀f s.
f has_bounded_variation_on s ⇔
(λx. f x) has_bounded_variation_on s
[HAS_BOUNDED_VARIATION_ON_COMPOSE_LINEAR] Theorem
⊢ ∀f g s.
f has_bounded_variation_on s ∧ linear g ⇒
g ∘ f has_bounded_variation_on s
[HAS_BOUNDED_VARIATION_ON_CONST] Theorem
⊢ ∀s c. (λx. c) has_bounded_variation_on s
[HAS_BOUNDED_VARIATION_ON_DIVISION] Theorem
⊢ ∀f a b d.
d division_of interval [(a,b)] ⇒
((∀k. k ∈ d ⇒ f has_bounded_variation_on k) ⇔
f has_bounded_variation_on interval [(a,b)])
[HAS_BOUNDED_VARIATION_ON_EMPTY] Theorem
⊢ ∀f. f has_bounded_variation_on ∅
[HAS_BOUNDED_VARIATION_ON_EQ] Theorem
⊢ ∀f g s.
(∀x. x ∈ s ⇒ f x = g x) ∧ f has_bounded_variation_on s ⇒
g has_bounded_variation_on s
[HAS_BOUNDED_VARIATION_ON_ID] Theorem
⊢ ∀a b. (λx. x) has_bounded_variation_on interval [(a,b)]
[HAS_BOUNDED_VARIATION_ON_IMP_BOUNDED] Theorem
⊢ ∀f s.
f has_bounded_variation_on s ∧ is_interval s ⇒
bounded (IMAGE f s)
[HAS_BOUNDED_VARIATION_ON_IMP_BOUNDED_ON_INTERVAL] Theorem
⊢ ∀f a b.
f has_bounded_variation_on interval [(a,b)] ⇒
bounded (IMAGE f (interval [(a,b)]))
[HAS_BOUNDED_VARIATION_ON_IMP_BOUNDED_ON_SUBINTERVALS] Theorem
⊢ ∀f s.
f has_bounded_variation_on s ⇒
bounded {f d − f c | interval [(c,d)] ⊆ s ∧ interval [(c,d)] ≠ ∅}
[HAS_BOUNDED_VARIATION_ON_INDEFINITE_INTEGRAL_LEFT] Theorem
⊢ ∀f a b.
f absolutely_integrable_on interval [(a,b)] ⇒
(λc. integral (interval [(c,b)]) f) has_bounded_variation_on
interval [(a,b)]
[HAS_BOUNDED_VARIATION_ON_INDEFINITE_INTEGRAL_RIGHT] Theorem
⊢ ∀f a b.
f absolutely_integrable_on interval [(a,b)] ⇒
(λc. integral (interval [(a,c)]) f) has_bounded_variation_on
interval [(a,b)]
[HAS_BOUNDED_VARIATION_ON_MAX] Theorem
⊢ ∀f g s.
f has_bounded_variation_on s ∧ g has_bounded_variation_on s ⇒
(λx. max (f x) (g x)) has_bounded_variation_on s
[HAS_BOUNDED_VARIATION_ON_MIN] Theorem
⊢ ∀f g s.
f has_bounded_variation_on s ∧ g has_bounded_variation_on s ⇒
(λx. min (f x) (g x)) has_bounded_variation_on s
[HAS_BOUNDED_VARIATION_ON_MUL] Theorem
⊢ ∀f g a b.
f has_bounded_variation_on interval [(a,b)] ∧
g has_bounded_variation_on interval [(a,b)] ⇒
(λx. f x * g x) has_bounded_variation_on interval [(a,b)]
[HAS_BOUNDED_VARIATION_ON_NEG] Theorem
⊢ ∀f s.
f has_bounded_variation_on s ⇒
(λx. -f x) has_bounded_variation_on s
[HAS_BOUNDED_VARIATION_ON_NULL] Theorem
⊢ ∀f s. content s = 0 ∧ bounded s ⇒ f has_bounded_variation_on s
[HAS_BOUNDED_VARIATION_ON_REFLECT] Theorem
⊢ ∀f s.
f has_bounded_variation_on IMAGE (λx. -x) s ⇒
(λx. f (-x)) has_bounded_variation_on s
[HAS_BOUNDED_VARIATION_ON_REFLECT_INTERVAL] Theorem
⊢ ∀f a b.
f has_bounded_variation_on interval [(-b,-a)] ⇒
(λx. f (-x)) has_bounded_variation_on interval [(a,b)]
[HAS_BOUNDED_VARIATION_ON_SING] Theorem
⊢ ∀f a. f has_bounded_variation_on {a}
[HAS_BOUNDED_VARIATION_ON_SUB] Theorem
⊢ ∀f g s.
f has_bounded_variation_on s ∧ g has_bounded_variation_on s ⇒
(λx. f x − g x) has_bounded_variation_on s
[HAS_BOUNDED_VARIATION_ON_SUBSET] Theorem
⊢ ∀f s t.
f has_bounded_variation_on s ∧ t ⊆ s ⇒
f has_bounded_variation_on t
[HAS_BOUNDED_VARIATION_ON_SUM] Theorem
⊢ ∀f s k.
FINITE k ∧ (∀i. i ∈ k ⇒ f i has_bounded_variation_on s) ⇒
(λx. sum k (λi. f i x)) has_bounded_variation_on s
[HAS_BOUNDED_VARIATION_ON_SUM_AND_SUM_LE] Theorem
⊢ (∀f s k.
FINITE k ∧ (∀i. i ∈ k ⇒ f i has_bounded_variation_on s) ⇒
(λx. sum k (λi. f i x)) has_bounded_variation_on s) ∧
∀f s k.
FINITE k ∧ (∀i. i ∈ k ⇒ f i has_bounded_variation_on s) ⇒
vector_variation s (λx. sum k (λi. f i x)) ≤
sum k (λi. vector_variation s (f i))
[HAS_BOUNDED_VARIATION_REFLECT2_EQ] Theorem
⊢ ∀f s.
(λx. f (-x)) has_bounded_variation_on IMAGE (λx. -x) s ⇔
f has_bounded_variation_on s
[HAS_BOUNDED_VARIATION_REFLECT2_EQ_AND_VECTOR_VARIATION_REFLECT2] Theorem
⊢ (∀f s.
(λx. f (-x)) has_bounded_variation_on IMAGE (λx. -x) s ⇔
f has_bounded_variation_on s) ∧
∀f s.
vector_variation (IMAGE (λx. -x) s) (λx. f (-x)) =
vector_variation s f
[HAS_BOUNDED_VARIATION_REFLECT_EQ] Theorem
⊢ ∀f s.
(λx. f (-x)) has_bounded_variation_on s ⇔
f has_bounded_variation_on IMAGE (λx. -x) s
[HAS_BOUNDED_VARIATION_REFLECT_EQ_AND_VECTOR_VARIATION_REFLECT] Theorem
⊢ (∀f s.
(λx. f (-x)) has_bounded_variation_on s ⇔
f has_bounded_variation_on IMAGE (λx. -x) s) ∧
∀f s.
vector_variation s (λx. f (-x)) =
vector_variation (IMAGE (λx. -x) s) f
[HAS_BOUNDED_VARIATION_REFLECT_EQ_INTERVAL] Theorem
⊢ ∀f u v.
(λx. f (-x)) has_bounded_variation_on interval [(u,v)] ⇔
f has_bounded_variation_on interval [(-v,-u)]
[HAS_BOUNDED_VARIATION_REFLECT_EQ_INTERVAL_AND_VECTOR_VARIATION_REFLECT_INTERVAL] Theorem
⊢ (∀f u v.
(λx. f (-x)) has_bounded_variation_on interval [(u,v)] ⇔
f has_bounded_variation_on interval [(-v,-u)]) ∧
∀f u v.
vector_variation (interval [(u,v)]) (λx. f (-x)) =
vector_variation (interval [(-v,-u)]) f
[HAS_BOUNDED_VARIATION_SUM_LE] Theorem
⊢ ∀f s k.
FINITE k ∧ (∀i. i ∈ k ⇒ f i has_bounded_variation_on s) ⇒
vector_variation s (λx. sum k (λi. f i x)) ≤
sum k (λi. vector_variation s (f i))
[HAS_BOUNDED_VARIATION_TRANSLATION] Theorem
⊢ ∀f s a.
f has_bounded_variation_on s ⇒
(λx. f (a + x)) has_bounded_variation_on IMAGE (λx. -a + x) s
[HAS_BOUNDED_VARIATION_TRANSLATION2_EQ] Theorem
⊢ ∀a f s.
(λx. f (a + x)) has_bounded_variation_on IMAGE (λx. -a + x) s ⇔
f has_bounded_variation_on s
[HAS_BOUNDED_VARIATION_TRANSLATION2_EQ_AND_VECTOR_VARIATION_TRANSLATION2] Theorem
⊢ (∀a f s.
(λx. f (a + x)) has_bounded_variation_on IMAGE (λx. -a + x) s ⇔
f has_bounded_variation_on s) ∧
∀a f s.
vector_variation (IMAGE (λx. -a + x) s) (λx. f (a + x)) =
vector_variation s f
[HAS_BOUNDED_VARIATION_TRANSLATION_EQ] Theorem
⊢ ∀a f s.
(λx. f (a + x)) has_bounded_variation_on s ⇔
f has_bounded_variation_on IMAGE (λx. a + x) s
[HAS_BOUNDED_VARIATION_TRANSLATION_EQ_AND_VECTOR_VARIATION_TRANSLATION] Theorem
⊢ (∀a f s.
(λx. f (a + x)) has_bounded_variation_on s ⇔
f has_bounded_variation_on IMAGE (λx. a + x) s) ∧
∀a f s.
vector_variation s (λx. f (a + x)) =
vector_variation (IMAGE (λx. a + x) s) f
[HAS_BOUNDED_VARIATION_TRANSLATION_EQ_INTERVAL] Theorem
⊢ ∀a f u v.
(λx. f (a + x)) has_bounded_variation_on interval [(u,v)] ⇔
f has_bounded_variation_on interval [(a + u,a + v)]
[HAS_BOUNDED_VARIATION_TRANSLATION_EQ_INTERVAL_AND_VECTOR_VARIATION_TRANSLATION_INTERVAL] Theorem
⊢ (∀a f u v.
(λx. f (a + x)) has_bounded_variation_on interval [(u,v)] ⇔
f has_bounded_variation_on interval [(a + u,a + v)]) ∧
∀a f u v.
vector_variation (interval [(u,v)]) (λx. f (a + x)) =
vector_variation (interval [(a + u,a + v)]) f
[HAS_BOUNDED_VECTOR_VARIATION_LEFT_LIMIT] Theorem
⊢ ∀f a b c.
f has_bounded_variation_on interval [(a,b)] ∧
c ∈ interval [(a,b)] ⇒
∃l. (f ⟶ l) (at c within interval [(a,c)])
[HAS_BOUNDED_VECTOR_VARIATION_RIGHT_LIMIT] Theorem
⊢ ∀f a b c.
f has_bounded_variation_on interval [(a,b)] ∧
c ∈ interval [(a,b)] ⇒
∃l. (f ⟶ l) (at c within interval [(c,b)])
[HAS_DERIVATIVE_ZERO_UNIQUE_STRONG_INTERVAL] Theorem
⊢ ∀f a b k y.
countable k ∧ f continuous_on interval [(a,b)] ∧ f a = y ∧
(∀x. x ∈ interval [(a,b)] DIFF k ⇒
(f has_derivative (λh. 0)) (at x within interval [(a,b)])) ⇒
∀x. x ∈ interval [(a,b)] ⇒ f x = y
[HAS_INTEGRAL] Theorem
⊢ ∀f i s.
(f has_integral i) s ⇔
∀e. 0 < e ⇒
∃B. 0 < B ∧
∀a b.
ball (0,B) ⊆ interval [(a,b)] ⇒
∃z. ((λx. if x ∈ s then f x else 0) has_integral z)
(interval [(a,b)]) ∧ abs (z − i) < e
[HAS_INTEGRAL_0] Theorem
⊢ ∀s. ((λx. 0) has_integral 0) s
[HAS_INTEGRAL_0_EQ] Theorem
⊢ ∀i s. ((λx. 0) has_integral i) s ⇔ i = 0
[HAS_INTEGRAL_ABS_BOUND_INTEGRAL_COMPONENT] Theorem
⊢ ∀f g s i j.
(f has_integral i) s ∧ (g has_integral j) s ∧
(∀x. x ∈ s ⇒ abs (f x) ≤ g x) ⇒
abs i ≤ j
[HAS_INTEGRAL_ADD] Theorem
⊢ ∀f g s k.
(f has_integral k) s ∧ (g has_integral l) s ⇒
((λx. f x + g x) has_integral k + l) s
[HAS_INTEGRAL_AFFINITY] Theorem
⊢ ∀f i a b m c.
(f has_integral i) (interval [(a,b)]) ∧ m ≠ 0 ⇒
((λx. f (m * x + c)) has_integral (abs m pow 1)⁻¹ * i)
(IMAGE (λx. m⁻¹ * x + -(m⁻¹ * c)) (interval [(a,b)]))
[HAS_INTEGRAL_ALT] Theorem
⊢ ∀f s i.
(f has_integral i) s ⇔
(∀a b.
(λx. if x ∈ s then f x else 0) integrable_on interval [(a,b)]) ∧
∀e. 0 < e ⇒
∃B. 0 < B ∧
∀a b.
ball (0,B) ⊆ interval [(a,b)] ⇒
abs
(integral (interval [(a,b)])
(λx. if x ∈ s then f x else 0) − i) < e
[HAS_INTEGRAL_BIGUNION] Theorem
⊢ ∀f i t.
FINITE t ∧ (∀s. s ∈ t ⇒ (f has_integral i s) s) ∧
(∀s s'. s ∈ t ∧ s' ∈ t ∧ s ≠ s' ⇒ negligible (s ∩ s')) ⇒
(f has_integral sum t i) (BIGUNION t)
[HAS_INTEGRAL_BOUND] Theorem
⊢ ∀f a b i B.
0 ≤ B ∧ (f has_integral i) (interval [(a,b)]) ∧
(∀x. x ∈ interval [(a,b)] ⇒ abs (f x) ≤ B) ⇒
abs i ≤ B * content (interval [(a,b)])
[HAS_INTEGRAL_CLOSURE] Theorem
⊢ ∀f y s.
negligible (frontier s) ⇒
((f has_integral y) (closure s) ⇔ (f has_integral y) s)
[HAS_INTEGRAL_CMUL] Theorem
⊢ ∀f k s c.
(f has_integral k) s ⇒ ((λx. c * f x) has_integral c * k) s
[HAS_INTEGRAL_COMBINE] Theorem
⊢ ∀f i j a b c.
a ≤ c ∧ c ≤ b ∧ (f has_integral i) (interval [(a,c)]) ∧
(f has_integral j) (interval [(c,b)]) ⇒
(f has_integral i + j) (interval [(a,b)])
[HAS_INTEGRAL_COMBINE_DIVISION] Theorem
⊢ ∀f s d i.
d division_of s ∧ (∀k. k ∈ d ⇒ (f has_integral i k) k) ⇒
(f has_integral sum d i) s
[HAS_INTEGRAL_COMBINE_DIVISION_TOPDOWN] Theorem
⊢ ∀f s d k.
f integrable_on s ∧ d division_of k ∧ k ⊆ s ⇒
(f has_integral sum d (λi. integral i f)) k
[HAS_INTEGRAL_COMBINE_TAGGED_DIVISION] Theorem
⊢ ∀f s p i.
p tagged_division_of s ∧
(∀x k. (x,k) ∈ p ⇒ (f has_integral i k) k) ⇒
(f has_integral sum p (λ(x,k). i k)) s
[HAS_INTEGRAL_COMBINE_TAGGED_DIVISION_TOPDOWN] Theorem
⊢ ∀f a b p.
f integrable_on interval [(a,b)] ∧
p tagged_division_of interval [(a,b)] ⇒
(f has_integral sum p (λ(x,k). integral k f)) (interval [(a,b)])
[HAS_INTEGRAL_COMPONENTWISE] Theorem
⊢ ∀f s y. (f has_integral y) s ⇔ ((λx. f x) has_integral y) s
[HAS_INTEGRAL_COMPONENT_LBOUND] Theorem
⊢ ∀f a b i.
(f has_integral i) (interval [(a,b)]) ∧
(∀x. x ∈ interval [(a,b)] ⇒ B ≤ f x) ⇒
B * content (interval [(a,b)]) ≤ i
[HAS_INTEGRAL_COMPONENT_LE] Theorem
⊢ ∀f g s i j.
(f has_integral i) s ∧ (g has_integral j) s ∧
(∀x. x ∈ s ⇒ f x ≤ g x) ⇒
i ≤ j
[HAS_INTEGRAL_COMPONENT_LE_AE] Theorem
⊢ ∀f g s i j k t.
negligible t ∧ (f has_integral i) s ∧ (g has_integral j) s ∧
(∀x. x ∈ s DIFF t ⇒ f x ≤ g x) ⇒
i ≤ j
[HAS_INTEGRAL_COMPONENT_NEG] Theorem
⊢ ∀f s i. (f has_integral i) s ∧ (∀x. x ∈ s ⇒ f x ≤ 0) ⇒ i ≤ 0
[HAS_INTEGRAL_COMPONENT_POS] Theorem
⊢ ∀f s i. (f has_integral i) s ∧ (∀x. x ∈ s ⇒ 0 ≤ f x) ⇒ 0 ≤ i
[HAS_INTEGRAL_COMPONENT_UBOUND] Theorem
⊢ ∀f a b i.
(f has_integral i) (interval [(a,b)]) ∧
(∀x. x ∈ interval [(a,b)] ⇒ f x ≤ B) ⇒
i ≤ B * content (interval [(a,b)])
[HAS_INTEGRAL_CONST] Theorem
⊢ ∀a b c.
((λx. c) has_integral content (interval [(a,b)]) * c)
(interval [(a,b)])
[HAS_INTEGRAL_DIFF] Theorem
⊢ ∀f i j s t.
(f has_integral i) s ∧ (f has_integral j) t ∧
negligible (t DIFF s) ⇒
(f has_integral i − j) (s DIFF t)
[HAS_INTEGRAL_DROP_LE] Theorem
⊢ ∀f g s i j.
(f has_integral i) s ∧ (g has_integral j) s ∧
(∀x. x ∈ s ⇒ f x ≤ g x) ⇒
i ≤ j
[HAS_INTEGRAL_DROP_NEG] Theorem
⊢ ∀f s i. (f has_integral i) s ∧ (∀x. x ∈ s ⇒ f x ≤ 0) ⇒ i ≤ 0
[HAS_INTEGRAL_DROP_POS] Theorem
⊢ ∀f s i. (f has_integral i) s ∧ (∀x. x ∈ s ⇒ 0 ≤ f x) ⇒ 0 ≤ i
[HAS_INTEGRAL_DROP_POS_AE] Theorem
⊢ ∀f s t i.
(f has_integral i) s ∧ negligible t ∧
(∀x. x ∈ s DIFF t ⇒ 0 ≤ f x) ⇒
0 ≤ i
[HAS_INTEGRAL_EMPTY] Theorem
⊢ ∀f. (f has_integral 0) ∅
[HAS_INTEGRAL_EMPTY_EQ] Theorem
⊢ ∀f i. (f has_integral i) ∅ ⇔ i = 0
[HAS_INTEGRAL_EQ] Theorem
⊢ ∀f g k s.
(∀x. x ∈ s ⇒ f x = g x) ∧ (f has_integral k) s ⇒
(g has_integral k) s
[HAS_INTEGRAL_EQ_EQ] Theorem
⊢ ∀f g k s.
(∀x. x ∈ s ⇒ f x = g x) ⇒
((f has_integral k) s ⇔ (g has_integral k) s)
[HAS_INTEGRAL_FACTOR_CONTENT] Theorem
⊢ ∀f i a b.
(f has_integral i) (interval [(a,b)]) ⇔
∀e. 0 < e ⇒
∃d. gauge d ∧
∀p. p tagged_division_of interval [(a,b)] ∧ d FINE p ⇒
abs (sum p (λ(x,k). content k * f x) − i) ≤
e * content (interval [(a,b)])
[HAS_INTEGRAL_INTEGRABLE] Theorem
⊢ ∀f i s. (f has_integral i) s ⇒ f integrable_on s
[HAS_INTEGRAL_INTEGRABLE_INTEGRAL] Theorem
⊢ ∀f i s. (f has_integral i) s ⇔ f integrable_on s ∧ integral s f = i
[HAS_INTEGRAL_INTEGRAL] Theorem
⊢ ∀f s. f integrable_on s ⇔ (f has_integral integral s f) s
[HAS_INTEGRAL_INTERIOR] Theorem
⊢ ∀f y s.
negligible (frontier s) ⇒
((f has_integral y) (interior s) ⇔ (f has_integral y) s)
[HAS_INTEGRAL_IS_0] Theorem
⊢ ∀f s. (∀x. x ∈ s ⇒ f x = 0) ⇒ (f has_integral 0) s
[HAS_INTEGRAL_LE_AE] Theorem
⊢ ∀f g s i j t.
(f has_integral i) s ∧ (g has_integral j) s ∧ negligible t ∧
(∀x. x ∈ s DIFF t ⇒ f x ≤ g x) ⇒
i ≤ j
[HAS_INTEGRAL_LIM_AT_POSINFINITY] Theorem
⊢ ∀f l.
(f has_integral l) {t | 0 ≤ t} ⇔
(∀a. f integrable_on interval [(0,a)]) ∧
((λa. integral (interval [(0,a)]) f) ⟶ l) at_posinfinity
[HAS_INTEGRAL_LIM_SEQUENTIALLY] Theorem
⊢ ∀f l.
(f ⟶ 0) at_posinfinity ∧
(∀n. f integrable_on interval [(0,&n)]) ∧
((λn. integral (interval [(0,&n)]) f) ⟶ l) sequentially ⇒
(f has_integral l) {t | 0 ≤ t}
[HAS_INTEGRAL_LINEAR] Theorem
⊢ ∀f y s h.
(f has_integral y) s ∧ linear h ⇒ (h ∘ f has_integral h y) s
[HAS_INTEGRAL_NEG] Theorem
⊢ ∀f k s. (f has_integral k) s ⇒ ((λx. -f x) has_integral -k) s
[HAS_INTEGRAL_NEGLIGIBLE] Theorem
⊢ ∀f s t.
negligible s ∧ (∀x. x ∈ t DIFF s ⇒ f x = 0) ⇒
(f has_integral 0) t
[HAS_INTEGRAL_NEGLIGIBLE_EQ] Theorem
⊢ ∀f s.
(∀x i. x ∈ s ⇒ 0 ≤ f x) ⇒
((f has_integral 0) s ⇔ negligible {x | x ∈ s ∧ f x ≠ 0})
[HAS_INTEGRAL_NULL] Theorem
⊢ ∀f a b.
content (interval [(a,b)]) = 0 ⇒
(f has_integral 0) (interval [(a,b)])
[HAS_INTEGRAL_NULL_EQ] Theorem
⊢ ∀f a b i.
content (interval [(a,b)]) = 0 ⇒
((f has_integral i) (interval [(a,b)]) ⇔ i = 0)
[HAS_INTEGRAL_ON_SUPERSET] Theorem
⊢ ∀f s t i.
(∀x. x ∉ s ⇒ f x = 0) ∧ s ⊆ t ∧ (f has_integral i) s ⇒
(f has_integral i) t
[HAS_INTEGRAL_REFL] Theorem
⊢ ∀f a. (f has_integral 0) (interval [(a,a)])
[HAS_INTEGRAL_REFLECT] Theorem
⊢ ∀f i a b.
((λx. f (-x)) has_integral i) (interval [(-b,-a)]) ⇔
(f has_integral i) (interval [(a,b)])
[HAS_INTEGRAL_REFLECT_GEN] Theorem
⊢ ∀f i s.
((λx. f (-x)) has_integral i) s ⇔
(f has_integral i) (IMAGE (λx. -x) s)
[HAS_INTEGRAL_REFLECT_LEMMA] Theorem
⊢ ∀f i a b.
(f has_integral i) (interval [(a,b)]) ⇒
((λx. f (-x)) has_integral i) (interval [(-b,-a)])
[HAS_INTEGRAL_RESTRICT] Theorem
⊢ ∀f s t i.
s ⊆ t ⇒
(((λx. if x ∈ s then f x else 0) has_integral i) t ⇔
(f has_integral i) s)
[HAS_INTEGRAL_RESTRICT_CLOSED_SUBINTERVAL] Theorem
⊢ ∀f a b c d i.
(f has_integral i) (interval [(c,d)]) ∧
interval [(c,d)] ⊆ interval [(a,b)] ⇒
((λx. if x ∈ interval [(c,d)] then f x else 0) has_integral i)
(interval [(a,b)])
[HAS_INTEGRAL_RESTRICT_CLOSED_SUBINTERVALS_EQ] Theorem
⊢ ∀f a b c d i.
interval [(c,d)] ⊆ interval [(a,b)] ⇒
(((λx. if x ∈ interval [(c,d)] then f x else 0) has_integral i)
(interval [(a,b)]) ⇔ (f has_integral i) (interval [(c,d)]))
[HAS_INTEGRAL_RESTRICT_INTER] Theorem
⊢ ∀f s t.
((λx. if x ∈ s then f x else 0) has_integral i) t ⇔
(f has_integral i) (s ∩ t)
[HAS_INTEGRAL_RESTRICT_OPEN_SUBINTERVAL] Theorem
⊢ ∀f a b c d i.
(f has_integral i) (interval [(c,d)]) ∧
interval [(c,d)] ⊆ interval [(a,b)] ⇒
((λx. if x ∈ interval (c,d) then f x else 0) has_integral i)
(interval [(a,b)])
[HAS_INTEGRAL_RESTRICT_UNIV] Theorem
⊢ ∀f s i.
((λx. if x ∈ s then f x else 0) has_integral i) 𝕌(:real) ⇔
(f has_integral i) s
[HAS_INTEGRAL_SEPARATE_SIDES] Theorem
⊢ ∀f i a b.
(f has_integral i) (interval [(a,b)]) ⇒
∀e. 0 < e ⇒
∃d. gauge d ∧
∀p1 p2.
p1 tagged_division_of interval [(a,b)] ∩ {x | x ≤ c} ∧
d FINE p1 ∧
p2 tagged_division_of interval [(a,b)] ∩ {x | x ≥ c} ∧
d FINE p2 ⇒
abs
(sum p1 (λ(x,k). content k * f x) +
sum p2 (λ(x,k). content k * f x) − i) < e
[HAS_INTEGRAL_SPIKE] Theorem
⊢ ∀f g s t y.
negligible s ∧ (∀x. x ∈ t DIFF s ⇒ g x = f x) ∧
(f has_integral y) t ⇒
(g has_integral y) t
[HAS_INTEGRAL_SPIKE_EQ] Theorem
⊢ ∀f g s t y.
negligible s ∧ (∀x. x ∈ t DIFF s ⇒ g x = f x) ⇒
((f has_integral y) t ⇔ (g has_integral y) t)
[HAS_INTEGRAL_SPIKE_FINITE] Theorem
⊢ ∀f g s t y.
FINITE s ∧ (∀x. x ∈ t DIFF s ⇒ g x = f x) ∧ (f has_integral y) t ⇒
(g has_integral y) t
[HAS_INTEGRAL_SPIKE_FINITE_EQ] Theorem
⊢ ∀f g s t y.
FINITE s ∧ (∀x. x ∈ t DIFF s ⇒ g x = f x) ⇒
((f has_integral y) t ⇔ (g has_integral y) t)
[HAS_INTEGRAL_SPIKE_INTERIOR] Theorem
⊢ ∀f g a b y.
(∀x. x ∈ interval (a,b) ⇒ g x = f x) ∧
(f has_integral y) (interval [(a,b)]) ⇒
(g has_integral y) (interval [(a,b)])
[HAS_INTEGRAL_SPIKE_INTERIOR_EQ] Theorem
⊢ ∀f g a b y.
(∀x. x ∈ interval (a,b) ⇒ g x = f x) ⇒
((f has_integral y) (interval [(a,b)]) ⇔
(g has_integral y) (interval [(a,b)]))
[HAS_INTEGRAL_SPIKE_SET] Theorem
⊢ ∀f s t y.
negligible (s DIFF t ∪ (t DIFF s)) ∧ (f has_integral y) s ⇒
(f has_integral y) t
[HAS_INTEGRAL_SPIKE_SET_EQ] Theorem
⊢ ∀f s t y.
negligible (s DIFF t ∪ (t DIFF s)) ⇒
((f has_integral y) s ⇔ (f has_integral y) t)
[HAS_INTEGRAL_SPLIT] Theorem
⊢ ∀f a b c.
(f has_integral i) (interval [(a,b)] ∩ {x | x ≤ c}) ∧
(f has_integral j) (interval [(a,b)] ∩ {x | x ≥ c}) ⇒
(f has_integral i + j) (interval [(a,b)])
[HAS_INTEGRAL_STRADDLE_NULL] Theorem
⊢ ∀f g s.
(∀x. x ∈ s ⇒ 0 ≤ f x ∧ f x ≤ g x) ∧ (g has_integral 0) s ⇒
(f has_integral 0) s
[HAS_INTEGRAL_STRETCH] Theorem
⊢ ∀f i m a b.
(f has_integral i) (interval [(a,b)]) ∧ m 1 ≠ 0 ⇒
((λx. f (m 1 * x)) has_integral (abs (product {1 .. 1} m))⁻¹ * i)
(IMAGE (λx. (m 1)⁻¹ * x) (interval [(a,b)]))
[HAS_INTEGRAL_SUB] Theorem
⊢ ∀f g s k l.
(f has_integral k) s ∧ (g has_integral l) s ⇒
((λx. f x − g x) has_integral k − l) s
[HAS_INTEGRAL_SUBSET_COMPONENT_LE] Theorem
⊢ ∀f s t i j.
s ⊆ t ∧ (f has_integral i) s ∧ (f has_integral j) t ∧
(∀x. x ∈ t ⇒ 0 ≤ f x) ⇒
i ≤ j
[HAS_INTEGRAL_SUBSET_DROP_LE] Theorem
⊢ ∀f s t i j.
s ⊆ t ∧ (f has_integral i) s ∧ (f has_integral j) t ∧
(∀x. x ∈ t ⇒ 0 ≤ f x) ⇒
i ≤ j
[HAS_INTEGRAL_SUM] Theorem
⊢ ∀f s t.
FINITE t ∧ (∀a. a ∈ t ⇒ (f a has_integral i a) s) ⇒
((λx. sum t (λa. f a x)) has_integral sum t i) s
[HAS_INTEGRAL_TWIDDLE] Theorem
⊢ ∀f g h r i a b.
0 < r ∧ (∀x. h (g x) = x) ∧ (∀x. g (h x) = x) ∧
(∀x. g continuous at x) ∧
(∀u v. ∃w z. IMAGE g (interval [(u,v)]) = interval [(w,z)]) ∧
(∀u v. ∃w z. IMAGE h (interval [(u,v)]) = interval [(w,z)]) ∧
(∀u v.
content (IMAGE g (interval [(u,v)])) =
r * content (interval [(u,v)])) ∧
(f has_integral i) (interval [(a,b)]) ⇒
((λx. f (g x)) has_integral r⁻¹ * i) (IMAGE h (interval [(a,b)]))
[HAS_INTEGRAL_UNION] Theorem
⊢ ∀f i j s t.
(f has_integral i) s ∧ (f has_integral j) t ∧ negligible (s ∩ t) ⇒
(f has_integral i + j) (s ∪ t)
[HAS_INTEGRAL_UNIQUE] Theorem
⊢ ∀f i k1 k2. (f has_integral k1) i ∧ (f has_integral k2) i ⇒ k1 = k2
[HENSTOCK_LEMMA] Theorem
⊢ ∀f a b.
f integrable_on interval [(a,b)] ⇒
∀e. 0 < e ⇒
∃d. gauge d ∧
∀p. p tagged_partial_division_of interval [(a,b)] ∧
d FINE p ⇒
sum p (λ(x,k). abs (content k * f x − integral k f)) <
e
[HENSTOCK_LEMMA_PART1] Theorem
⊢ ∀f a b d e.
f integrable_on interval [(a,b)] ∧ 0 < e ∧ gauge d ∧
(∀p. p tagged_division_of interval [(a,b)] ∧ d FINE p ⇒
abs
(sum p (λ(x,k). content k * f x) −
integral (interval [(a,b)]) f) < e) ⇒
∀p. p tagged_partial_division_of interval [(a,b)] ∧ d FINE p ⇒
abs (sum p (λ(x,k). content k * f x − integral k f)) ≤ e
[HENSTOCK_LEMMA_PART2] Theorem
⊢ ∀f a b d e.
f integrable_on interval [(a,b)] ∧ 0 < e ∧ gauge d ∧
(∀p. p tagged_division_of interval [(a,b)] ∧ d FINE p ⇒
abs
(sum p (λ(x,k). content k * f x) −
integral (interval [(a,b)]) f) < e) ⇒
∀p. p tagged_partial_division_of interval [(a,b)] ∧ d FINE p ⇒
sum p (λ(x,k). abs (content k * f x − integral k f)) ≤
2 * 1 * e
[INCREASING_BOUNDED_VARIATION] Theorem
⊢ ∀f a b.
(∀x y.
x ∈ interval [(a,b)] ∧ y ∈ interval [(a,b)] ∧ x ≤ y ⇒
f x ≤ f y) ⇒
f has_bounded_variation_on interval [(a,b)]
[INCREASING_BOUNDED_VARIATION_GEN] Theorem
⊢ ∀f s.
bounded (IMAGE f s) ∧ (∀x y. x ∈ s ∧ y ∈ s ∧ x ≤ y ⇒ f x ≤ f y) ⇒
f has_bounded_variation_on s
[INCREASING_LEFT_LIMIT] Theorem
⊢ ∀f a b c.
(∀x y.
x ∈ interval [(a,b)] ∧ y ∈ interval [(a,b)] ∧ x ≤ y ⇒
f x ≤ f y) ∧ c ∈ interval [(a,b)] ⇒
∃l. (f ⟶ l) (at c within interval [(a,c)])
[INCREASING_RIGHT_LIMIT] Theorem
⊢ ∀f a b c.
(∀x y.
x ∈ interval [(a,b)] ∧ y ∈ interval [(a,b)] ∧ x ≤ y ⇒
f x ≤ f y) ∧ c ∈ interval [(a,b)] ⇒
∃l. (f ⟶ l) (at c within interval [(c,b)])
[INCREASING_VECTOR_VARIATION] Theorem
⊢ ∀f a b.
interval [(a,b)] ≠ ∅ ∧
(∀x y.
x ∈ interval [(a,b)] ∧ y ∈ interval [(a,b)] ∧ x ≤ y ⇒
f x ≤ f y) ⇒
vector_variation (interval [(a,b)]) f = f b − f a
[INDEFINITE_INTEGRAL_CONTINUOUS] Theorem
⊢ ∀f a b c d e.
f integrable_on interval [(a,b)] ∧ c ∈ interval [(a,b)] ∧
d ∈ interval [(a,b)] ∧ 0 < e ⇒
∃k. 0 < k ∧
∀c' d'.
c' ∈ interval [(a,b)] ∧ d' ∈ interval [(a,b)] ∧
abs (c' − c) ≤ k ∧ abs (d' − d) ≤ k ⇒
abs
(integral (interval [(c',d')]) f −
integral (interval [(c,d)]) f) < e
[INDEFINITE_INTEGRAL_CONTINUOUS_LEFT] Theorem
⊢ ∀f a b.
f integrable_on interval [(a,b)] ⇒
(λx. integral (interval [(x,b)]) f) continuous_on
interval [(a,b)]
[INDEFINITE_INTEGRAL_CONTINUOUS_RIGHT] Theorem
⊢ ∀f a b.
f integrable_on interval [(a,b)] ⇒
(λx. integral (interval [(a,x)]) f) continuous_on
interval [(a,b)]
[INTEGRABLE_0] Theorem
⊢ ∀s. (λx. 0) integrable_on s
[INTEGRABLE_ADD] Theorem
⊢ ∀f g s.
f integrable_on s ∧ g integrable_on s ⇒
(λx. f x + g x) integrable_on s
[INTEGRABLE_AFFINITY] Theorem
⊢ ∀f a b m c.
f integrable_on interval [(a,b)] ∧ m ≠ 0 ⇒
(λx. f (m * x + c)) integrable_on
IMAGE (λx. m⁻¹ * x + -(m⁻¹ * c)) (interval [(a,b)])
[INTEGRABLE_ALT] Theorem
⊢ ∀f s.
f integrable_on s ⇔
(∀a b.
(λx. if x ∈ s then f x else 0) integrable_on interval [(a,b)]) ∧
∀e. 0 < e ⇒
∃B. 0 < B ∧
∀a b c d.
ball (0,B) ⊆ interval [(a,b)] ∧
ball (0,B) ⊆ interval [(c,d)] ⇒
abs
(integral (interval [(a,b)])
(λx. if x ∈ s then f x else 0) −
integral (interval [(c,d)])
(λx. if x ∈ s then f x else 0)) < e
[INTEGRABLE_ALT_SUBSET] Theorem
⊢ ∀f s.
f integrable_on s ⇔
(∀a b.
(λx. if x ∈ s then f x else 0) integrable_on interval [(a,b)]) ∧
∀e. 0 < e ⇒
∃B. 0 < B ∧
∀a b c d.
ball (0,B) ⊆ interval [(a,b)] ∧
interval [(a,b)] ⊆ interval [(c,d)] ⇒
abs
(integral (interval [(a,b)])
(λx. if x ∈ s then f x else 0) −
integral (interval [(c,d)])
(λx. if x ∈ s then f x else 0)) < e
[INTEGRABLE_BOUNDED_VARIATION] Theorem
⊢ ∀f a b.
f has_bounded_variation_on interval [(a,b)] ⇒
f integrable_on interval [(a,b)]
[INTEGRABLE_BOUNDED_VARIATION_BILINEAR_LMUL] Theorem
⊢ ∀op f g a b.
bilinear op ∧ f integrable_on interval [(a,b)] ∧
g has_bounded_variation_on interval [(a,b)] ⇒
(λx. op (g x) (f x)) integrable_on interval [(a,b)]
[INTEGRABLE_BOUNDED_VARIATION_BILINEAR_RMUL] Theorem
⊢ ∀op f g a b.
bilinear op ∧ f integrable_on interval [(a,b)] ∧
g has_bounded_variation_on interval [(a,b)] ⇒
(λx. op (f x) (g x)) integrable_on interval [(a,b)]
[INTEGRABLE_BOUNDED_VARIATION_PRODUCT] Theorem
⊢ ∀f g a b.
f integrable_on interval [(a,b)] ∧
g has_bounded_variation_on interval [(a,b)] ⇒
(λx. g x * f x) integrable_on interval [(a,b)]
[INTEGRABLE_BOUNDED_VARIATION_PRODUCT_ALT] Theorem
⊢ ∀f g a b.
f integrable_on interval [(a,b)] ∧
g has_bounded_variation_on interval [(a,b)] ⇒
(λx. g x * f x) integrable_on interval [(a,b)]
[INTEGRABLE_BY_PARTS] Theorem
⊢ ∀bop f g f' g' a b c.
bilinear bop ∧ countable c ∧
(λx. bop (f x) (g x)) continuous_on interval [(a,b)] ∧
(∀x. x ∈ interval (a,b) DIFF c ⇒
(f has_vector_derivative f' x) (at x) ∧
(g has_vector_derivative g' x) (at x)) ∧
(λx. bop (f x) (g' x)) integrable_on interval [(a,b)] ⇒
(λx. bop (f' x) (g x)) integrable_on interval [(a,b)]
[INTEGRABLE_BY_PARTS_EQ] Theorem
⊢ ∀bop f g f' g' a b c.
bilinear bop ∧ countable c ∧
(λx. bop (f x) (g x)) continuous_on interval [(a,b)] ∧
(∀x. x ∈ interval (a,b) DIFF c ⇒
(f has_vector_derivative f' x) (at x) ∧
(g has_vector_derivative g' x) (at x)) ⇒
((λx. bop (f x) (g' x)) integrable_on interval [(a,b)] ⇔
(λx. bop (f' x) (g x)) integrable_on interval [(a,b)])
[INTEGRABLE_CASES] Theorem
⊢ ∀P f g s.
f integrable_on {x | x ∈ s ∧ P x} ∧
g integrable_on {x | x ∈ s ∧ ¬P x} ⇒
(λx. if P x then f x else g x) integrable_on s
[INTEGRABLE_CAUCHY] Theorem
⊢ ∀f a b.
f integrable_on interval [(a,b)] ⇔
∀e. 0 < e ⇒
∃d. gauge d ∧
∀p1 p2.
p1 tagged_division_of interval [(a,b)] ∧ d FINE p1 ∧
p2 tagged_division_of interval [(a,b)] ∧ d FINE p2 ⇒
abs
(sum p1 (λ(x,k). content k * f x) −
sum p2 (λ(x,k). content k * f x)) < e
[INTEGRABLE_CMUL] Theorem
⊢ ∀f c s. f integrable_on s ⇒ (λx. c * f x) integrable_on s
[INTEGRABLE_CMUL_EQ] Theorem
⊢ ∀f s c. (λx. c * f x) integrable_on s ⇔ c = 0 ∨ f integrable_on s
[INTEGRABLE_COMBINE] Theorem
⊢ ∀f a b c.
a ≤ c ∧ c ≤ b ∧ f integrable_on interval [(a,c)] ∧
f integrable_on interval [(c,b)] ⇒
f integrable_on interval [(a,b)]
[INTEGRABLE_COMBINE_DIVISION] Theorem
⊢ ∀f d s.
d division_of s ∧ (∀i. i ∈ d ⇒ f integrable_on i) ⇒
f integrable_on s
[INTEGRABLE_COMPONENTWISE] Theorem
⊢ ∀f s. f integrable_on s ⇔ (λx. f x) integrable_on s
[INTEGRABLE_CONST] Theorem
⊢ ∀a b c. (λx. c) integrable_on interval [(a,b)]
[INTEGRABLE_CONTINUOUS] Theorem
⊢ ∀f a b.
f continuous_on interval [(a,b)] ⇒
f integrable_on interval [(a,b)]
[INTEGRABLE_DECREASING] Theorem
⊢ ∀f a b.
(∀x y i.
x ∈ interval [(a,b)] ∧ y ∈ interval [(a,b)] ∧ x ≤ y ⇒
f y ≤ f x) ⇒
f integrable_on interval [(a,b)]
[INTEGRABLE_DECREASING_PRODUCT] Theorem
⊢ ∀f g a b.
f integrable_on interval [(a,b)] ∧
(∀x y.
x ∈ interval [(a,b)] ∧ y ∈ interval [(a,b)] ∧ x ≤ y ⇒
g y ≤ g x) ⇒
(λx. g x * f x) integrable_on interval [(a,b)]
[INTEGRABLE_DECREASING_PRODUCT_UNIV] Theorem
⊢ ∀f g B.
f integrable_on 𝕌(:real) ∧ (∀x y. x ≤ y ⇒ g y ≤ g x) ∧
(∀x. abs (g x) ≤ B) ⇒
(λx. g x * f x) integrable_on 𝕌(:real)
[INTEGRABLE_EQ] Theorem
⊢ ∀f g s.
(∀x. x ∈ s ⇒ f x = g x) ∧ f integrable_on s ⇒ g integrable_on s
[INTEGRABLE_INCREASING] Theorem
⊢ ∀f a b.
(∀x y i.
x ∈ interval [(a,b)] ∧ y ∈ interval [(a,b)] ∧ x ≤ y ⇒
f x ≤ f y) ⇒
f integrable_on interval [(a,b)]
[INTEGRABLE_INCREASING_PRODUCT] Theorem
⊢ ∀f g a b.
f integrable_on interval [(a,b)] ∧
(∀x y.
x ∈ interval [(a,b)] ∧ y ∈ interval [(a,b)] ∧ x ≤ y ⇒
g x ≤ g y) ⇒
(λx. g x * f x) integrable_on interval [(a,b)]
[INTEGRABLE_INCREASING_PRODUCT_UNIV] Theorem
⊢ ∀f g B.
f integrable_on 𝕌(:real) ∧ (∀x y. x ≤ y ⇒ g x ≤ g y) ∧
(∀x. abs (g x) ≤ B) ⇒
(λx. g x * f x) integrable_on 𝕌(:real)
[INTEGRABLE_INTEGRAL] Theorem
⊢ ∀f i. f integrable_on i ⇒ (f has_integral integral i f) i
[INTEGRABLE_LINEAR] Theorem
⊢ ∀f h s. f integrable_on s ∧ linear h ⇒ h ∘ f integrable_on s
[INTEGRABLE_MIN_CONST] Theorem
⊢ ∀f s t.
0 ≤ t ∧ (∀x. x ∈ s ⇒ 0 ≤ f x) ∧ (λx. f x) integrable_on s ⇒
(λx. min (f x) t) integrable_on s
[INTEGRABLE_NEG] Theorem
⊢ ∀f s. f integrable_on s ⇒ (λx. -f x) integrable_on s
[INTEGRABLE_ON_ALL_INTERVALS_INTEGRABLE_BOUND] Theorem
⊢ ∀f g s.
(∀a b.
(λx. if x ∈ s then f x else 0) integrable_on interval [(a,b)]) ∧
(∀x. x ∈ s ⇒ abs (f x) ≤ g x) ∧ g integrable_on s ⇒
f integrable_on s
[INTEGRABLE_ON_EMPTY] Theorem
⊢ ∀f. f integrable_on ∅
[INTEGRABLE_ON_LITTLE_SUBINTERVALS] Theorem
⊢ ∀f a b.
(∀x. x ∈ interval [(a,b)] ⇒
∃d. 0 < d ∧
∀u v.
x ∈ interval [(u,v)] ∧ interval [(u,v)] ⊆ ball (x,d) ∧
interval [(u,v)] ⊆ interval [(a,b)] ⇒
f integrable_on interval [(u,v)]) ⇒
f integrable_on interval [(a,b)]
[INTEGRABLE_ON_NULL] Theorem
⊢ ∀f a b.
content (interval [(a,b)]) = 0 ⇒ f integrable_on interval [(a,b)]
[INTEGRABLE_ON_REFL] Theorem
⊢ ∀f a. f integrable_on interval [(a,a)]
[INTEGRABLE_ON_SUBDIVISION] Theorem
⊢ ∀f s d i.
d division_of i ∧ f integrable_on s ∧ i ⊆ s ⇒ f integrable_on i
[INTEGRABLE_ON_SUBINTERVAL] Theorem
⊢ ∀f s a b.
f integrable_on s ∧ interval [(a,b)] ⊆ s ⇒
f integrable_on interval [(a,b)]
[INTEGRABLE_ON_SUPERSET] Theorem
⊢ ∀f s t.
(∀x. x ∉ s ⇒ f x = 0) ∧ s ⊆ t ∧ f integrable_on s ⇒
f integrable_on t
[INTEGRABLE_REFLECT] Theorem
⊢ ∀f a b.
(λx. f (-x)) integrable_on interval [(-b,-a)] ⇔
f integrable_on interval [(a,b)]
[INTEGRABLE_REFLECT_GEN] Theorem
⊢ ∀f s.
(λx. f (-x)) integrable_on s ⇔ f integrable_on IMAGE (λx. -x) s
[INTEGRABLE_RESTRICT] Theorem
⊢ ∀f s t.
s ⊆ t ⇒
((λx. if x ∈ s then f x else 0) integrable_on t ⇔
f integrable_on s)
[INTEGRABLE_RESTRICT_INTER] Theorem
⊢ ∀f s t.
(λx. if x ∈ s then f x else 0) integrable_on t ⇔
f integrable_on s ∩ t
[INTEGRABLE_RESTRICT_UNIV] Theorem
⊢ ∀f s.
(λx. if x ∈ s then f x else 0) integrable_on 𝕌(:real) ⇔
f integrable_on s
[INTEGRABLE_SPIKE] Theorem
⊢ ∀f g s t.
negligible s ∧ (∀x. x ∈ t DIFF s ⇒ g x = f x) ⇒
f integrable_on t ⇒
g integrable_on t
[INTEGRABLE_SPIKE_EQ] Theorem
⊢ ∀f g s t.
negligible s ∧ (∀x. x ∈ t DIFF s ⇒ g x = f x) ⇒
(f integrable_on t ⇔ g integrable_on t)
[INTEGRABLE_SPIKE_FINITE] Theorem
⊢ ∀f g s.
FINITE s ∧ (∀x. x ∈ t DIFF s ⇒ g x = f x) ⇒
f integrable_on t ⇒
g integrable_on t
[INTEGRABLE_SPIKE_INTERIOR] Theorem
⊢ ∀f g a b.
(∀x. x ∈ interval (a,b) ⇒ g x = f x) ⇒
f integrable_on interval [(a,b)] ⇒
g integrable_on interval [(a,b)]
[INTEGRABLE_SPIKE_SET] Theorem
⊢ ∀f s t.
negligible (s DIFF t ∪ (t DIFF s)) ⇒
f integrable_on s ⇒
f integrable_on t
[INTEGRABLE_SPIKE_SET_EQ] Theorem
⊢ ∀f s t.
negligible (s DIFF t ∪ (t DIFF s)) ⇒
(f integrable_on s ⇔ f integrable_on t)
[INTEGRABLE_SPLIT] Theorem
⊢ ∀f a b.
f integrable_on interval [(a,b)] ⇒
f integrable_on interval [(a,b)] ∩ {x | x ≤ c} ∧
f integrable_on interval [(a,b)] ∩ {x | x ≥ c}
[INTEGRABLE_STRADDLE] Theorem
⊢ ∀f s.
(∀e. 0 < e ⇒
∃g h i j.
(g has_integral i) s ∧ (h has_integral j) s ∧
abs (i − j) < e ∧ ∀x. x ∈ s ⇒ g x ≤ f x ∧ f x ≤ h x) ⇒
f integrable_on s
[INTEGRABLE_STRADDLE_INTERVAL] Theorem
⊢ ∀f a b.
(∀e. 0 < e ⇒
∃g h i j.
(g has_integral i) (interval [(a,b)]) ∧
(h has_integral j) (interval [(a,b)]) ∧ abs (i − j) < e ∧
∀x. x ∈ interval [(a,b)] ⇒ g x ≤ f x ∧ f x ≤ h x) ⇒
f integrable_on interval [(a,b)]
[INTEGRABLE_STRETCH] Theorem
⊢ ∀f m a b.
f integrable_on interval [(a,b)] ∧ m 1 ≠ 0 ⇒
(λx. f (m 1 * x)) integrable_on
IMAGE (λx. (m 1)⁻¹ * x) (interval [(a,b)])
[INTEGRABLE_SUB] Theorem
⊢ ∀f g s.
f integrable_on s ∧ g integrable_on s ⇒
(λx. f x − g x) integrable_on s
[INTEGRABLE_SUBINTERVAL] Theorem
⊢ ∀f a b c d.
f integrable_on interval [(a,b)] ∧
interval [(c,d)] ⊆ interval [(a,b)] ⇒
f integrable_on interval [(c,d)]
[INTEGRABLE_SUM] Theorem
⊢ ∀f s t.
FINITE t ∧ (∀a. a ∈ t ⇒ f a integrable_on s) ⇒
(λx. sum t (λa. f a x)) integrable_on s
[INTEGRABLE_UNIFORM_LIMIT] Theorem
⊢ ∀f a b.
(∀e. 0 < e ⇒
∃g. (∀x. x ∈ interval [(a,b)] ⇒ abs (f x − g x) ≤ e) ∧
g integrable_on interval [(a,b)]) ⇒
f integrable_on interval [(a,b)]
[INTEGRAL_0] Theorem
⊢ ∀s. integral s (λx. 0) = 0
[INTEGRAL_ABS_BOUND_INTEGRAL] Theorem
⊢ ∀f g s.
f integrable_on s ∧ g integrable_on s ∧
(∀x. x ∈ s ⇒ abs (f x) ≤ g x) ⇒
abs (integral s f) ≤ integral s g
[INTEGRAL_ABS_BOUND_INTEGRAL_AE] Theorem
⊢ ∀f g s t.
f integrable_on s ∧ g integrable_on s ∧ negligible t ∧
(∀x. x ∈ s DIFF t ⇒ abs (f x) ≤ g x) ⇒
abs (integral s f) ≤ integral s g
[INTEGRAL_ABS_BOUND_INTEGRAL_COMPONENT] Theorem
⊢ ∀f g s.
f integrable_on s ∧ g integrable_on s ∧
(∀x. x ∈ s ⇒ abs (f x) ≤ g x) ⇒
abs (integral s f) ≤ integral s g
[INTEGRAL_ADD] Theorem
⊢ ∀f g s.
f integrable_on s ∧ g integrable_on s ⇒
integral s (λx. f x + g x) = integral s f + integral s g
[INTEGRAL_CMUL] Theorem
⊢ ∀f c s.
f integrable_on s ⇒ integral s (λx. c * f x) = c * integral s f
[INTEGRAL_COMBINE] Theorem
⊢ ∀f a b c.
a ≤ c ∧ c ≤ b ∧ f integrable_on interval [(a,b)] ⇒
integral (interval [(a,c)]) f + integral (interval [(c,b)]) f =
integral (interval [(a,b)]) f
[INTEGRAL_COMBINE_DIVISION_BOTTOMUP] Theorem
⊢ ∀f d s.
d division_of s ∧ (∀k. k ∈ d ⇒ f integrable_on k) ⇒
integral s f = sum d (λi. integral i f)
[INTEGRAL_COMBINE_DIVISION_TOPDOWN] Theorem
⊢ ∀f d s.
f integrable_on s ∧ d division_of s ⇒
integral s f = sum d (λi. integral i f)
[INTEGRAL_COMBINE_TAGGED_DIVISION_BOTTOMUP] Theorem
⊢ ∀f p a b.
p tagged_division_of interval [(a,b)] ∧
(∀x k. (x,k) ∈ p ⇒ f integrable_on k) ⇒
integral (interval [(a,b)]) f = sum p (λ(x,k). integral k f)
[INTEGRAL_COMBINE_TAGGED_DIVISION_TOPDOWN] Theorem
⊢ ∀f a b p.
f integrable_on interval [(a,b)] ∧
p tagged_division_of interval [(a,b)] ⇒
integral (interval [(a,b)]) f = sum p (λ(x,k). integral k f)
[INTEGRAL_COMPONENT] Theorem
⊢ ∀f s. f integrable_on s ⇒ integral s f = integral s (λx. f x)
[INTEGRAL_COMPONENT_LBOUND] Theorem
⊢ ∀f a b.
f integrable_on interval [(a,b)] ∧
(∀x. x ∈ interval [(a,b)] ⇒ B ≤ f x) ⇒
B * content (interval [(a,b)]) ≤ integral (interval [(a,b)]) f
[INTEGRAL_COMPONENT_LE] Theorem
⊢ ∀f g s.
f integrable_on s ∧ g integrable_on s ∧ (∀x. x ∈ s ⇒ f x ≤ g x) ⇒
integral s f ≤ integral s g
[INTEGRAL_COMPONENT_LE_AE] Theorem
⊢ ∀f g s k t.
negligible t ∧ f integrable_on s ∧ g integrable_on s ∧
(∀x. x ∈ s DIFF t ⇒ f x ≤ g x) ⇒
integral s f ≤ integral s g
[INTEGRAL_COMPONENT_POS] Theorem
⊢ ∀f s. f integrable_on s ∧ (∀x. x ∈ s ⇒ 0 ≤ f x) ⇒ 0 ≤ integral s f
[INTEGRAL_COMPONENT_UBOUND] Theorem
⊢ ∀f a b.
f integrable_on interval [(a,b)] ∧
(∀x. x ∈ interval [(a,b)] ⇒ f x ≤ B) ⇒
integral (interval [(a,b)]) f ≤ B * content (interval [(a,b)])
[INTEGRAL_CONST] Theorem
⊢ ∀a b c.
integral (interval [(a,b)]) (λx. c) =
content (interval [(a,b)]) * c
[INTEGRAL_DIFF] Theorem
⊢ ∀f s t.
f integrable_on s ∧ f integrable_on t ∧ negligible (t DIFF s) ⇒
integral (s DIFF t) f = integral s f − integral t f
[INTEGRAL_DROP_LE] Theorem
⊢ ∀f g s.
f integrable_on s ∧ g integrable_on s ∧ (∀x. x ∈ s ⇒ f x ≤ g x) ⇒
integral s f ≤ integral s g
[INTEGRAL_DROP_POS] Theorem
⊢ ∀f s. f integrable_on s ∧ (∀x. x ∈ s ⇒ 0 ≤ f x) ⇒ 0 ≤ integral s f
[INTEGRAL_DROP_POS_AE] Theorem
⊢ ∀f s t.
f integrable_on s ∧ negligible t ∧ (∀x. x ∈ s DIFF t ⇒ 0 ≤ f x) ⇒
0 ≤ integral s f
[INTEGRAL_EMPTY] Theorem
⊢ ∀f. integral ∅ f = 0
[INTEGRAL_EQ] Theorem
⊢ ∀f g s. (∀x. x ∈ s ⇒ f x = g x) ⇒ integral s f = integral s g
[INTEGRAL_EQ_0] Theorem
⊢ ∀f s. (∀x. x ∈ s ⇒ f x = 0) ⇒ integral s f = 0
[INTEGRAL_EQ_HAS_INTEGRAL] Theorem
⊢ ∀s f y.
f integrable_on s ⇒ (integral s f = y ⇔ (f has_integral y) s)
[INTEGRAL_HAS_VECTOR_DERIVATIVE] Theorem
⊢ ∀f a b.
f continuous_on interval [(a,b)] ⇒
∀x. x ∈ interval [(a,b)] ⇒
((λu. integral (interval [(a,u)]) f) has_vector_derivative
f x) (at x within interval [(a,b)])
[INTEGRAL_HAS_VECTOR_DERIVATIVE_POINTWISE] Theorem
⊢ ∀f a b x.
f integrable_on interval [(a,b)] ∧ x ∈ interval [(a,b)] ∧
f continuous (at x within interval [(a,b)]) ⇒
((λu. integral (interval [(a,u)]) f) has_vector_derivative f x)
(at x within interval [(a,b)])
[INTEGRAL_LE_AE] Theorem
⊢ ∀f g s t.
f integrable_on s ∧ g integrable_on s ∧ negligible t ∧
(∀x. x ∈ s DIFF t ⇒ f x ≤ g x) ⇒
integral s f ≤ integral s g
[INTEGRAL_LINEAR] Theorem
⊢ ∀f s h.
f integrable_on s ∧ linear h ⇒
integral s (h ∘ f) = h (integral s f)
[INTEGRAL_NEG] Theorem
⊢ ∀f s. f integrable_on s ⇒ integral s (λx. -f x) = -integral s f
[INTEGRAL_NULL] Theorem
⊢ ∀f a b.
content (interval [(a,b)]) = 0 ⇒
integral (interval [(a,b)]) f = 0
[INTEGRAL_REFL] Theorem
⊢ ∀f a. integral (interval [(a,a)]) f = 0
[INTEGRAL_REFLECT] Theorem
⊢ ∀f a b.
integral (interval [(-b,-a)]) (λx. f (-x)) =
integral (interval [(a,b)]) f
[INTEGRAL_REFLECT_GEN] Theorem
⊢ ∀f s. integral s (λx. f (-x)) = integral (IMAGE (λx. -x) s) f
[INTEGRAL_RESTRICT] Theorem
⊢ ∀f s t.
s ⊆ t ⇒ integral t (λx. if x ∈ s then f x else 0) = integral s f
[INTEGRAL_RESTRICT_INTER] Theorem
⊢ ∀f s t.
integral t (λx. if x ∈ s then f x else 0) = integral (s ∩ t) f
[INTEGRAL_RESTRICT_UNIV] Theorem
⊢ ∀f s.
integral 𝕌(:real) (λx. if x ∈ s then f x else 0) = integral s f
[INTEGRAL_SPIKE] Theorem
⊢ ∀f g s t y.
negligible s ∧ (∀x. x ∈ t DIFF s ⇒ g x = f x) ⇒
integral t f = integral t g
[INTEGRAL_SPIKE_SET] Theorem
⊢ ∀f s t.
negligible (s DIFF t ∪ (t DIFF s)) ⇒ integral s f = integral t f
[INTEGRAL_SPLIT] Theorem
⊢ ∀f a b t.
f integrable_on interval [(a,b)] ⇒
integral (interval [(a,b)]) f =
integral (interval [(a,@f. f = min b t)]) f +
integral (interval [((@f. f = max a t),b)]) f
[INTEGRAL_SPLIT_SIGNED] Theorem
⊢ ∀f a b t.
a ≤ t ∧ a ≤ b ∧ f integrable_on interval [(a,@f. f = max b t)] ⇒
integral (interval [(a,b)]) f =
integral (interval [(a,@f. f = t)]) f +
(if b < t then -1 else 1) *
integral (interval [((@f. f = min b t),@f. f = max b t)]) f
[INTEGRAL_SUB] Theorem
⊢ ∀f g k l s.
f integrable_on s ∧ g integrable_on s ⇒
integral s (λx. f x − g x) = integral s f − integral s g
[INTEGRAL_SUBSET_COMPONENT_LE] Theorem
⊢ ∀f s t.
s ⊆ t ∧ f integrable_on s ∧ f integrable_on t ∧
(∀x. x ∈ t ⇒ 0 ≤ f x) ⇒
integral s f ≤ integral t f
[INTEGRAL_SUBSET_DROP_LE] Theorem
⊢ ∀f s t.
s ⊆ t ∧ f integrable_on s ∧ f integrable_on t ∧
(∀x. x ∈ t ⇒ 0 ≤ f x) ⇒
integral s f ≤ integral t f
[INTEGRAL_SUM] Theorem
⊢ ∀f s t.
FINITE t ∧ (∀a. a ∈ t ⇒ f a integrable_on s) ⇒
integral s (λx. sum t (λa. f a x)) = sum t (λa. integral s (f a))
[INTEGRAL_UNION] Theorem
⊢ ∀f s t.
f integrable_on s ∧ f integrable_on t ∧ negligible (s ∩ t) ⇒
integral (s ∪ t) f = integral s f + integral t f
[INTEGRAL_UNIQUE] Theorem
⊢ ∀f y k. (f has_integral y) k ⇒ integral k f = y
[INTEGRATION_BY_PARTS] Theorem
⊢ ∀bop f g f' g' a b c y.
bilinear bop ∧ a ≤ b ∧ countable c ∧
(λx. bop (f x) (g x)) continuous_on interval [(a,b)] ∧
(∀x. x ∈ interval (a,b) DIFF c ⇒
(f has_vector_derivative f' x) (at x) ∧
(g has_vector_derivative g' x) (at x)) ∧
((λx. bop (f x) (g' x)) has_integral
bop (f b) (g b) − bop (f a) (g a) − y) (interval [(a,b)]) ⇒
((λx. bop (f' x) (g x)) has_integral y) (interval [(a,b)])
[INTEGRATION_BY_PARTS_SIMPLE] Theorem
⊢ ∀bop f g f' g' a b y.
bilinear bop ∧ a ≤ b ∧
(∀x. x ∈ interval [(a,b)] ⇒
(f has_vector_derivative f' x)
(at x within interval [(a,b)]) ∧
(g has_vector_derivative g' x)
(at x within interval [(a,b)])) ∧
((λx. bop (f x) (g' x)) has_integral
bop (f b) (g b) − bop (f a) (g a) − y) (interval [(a,b)]) ⇒
((λx. bop (f' x) (g x)) has_integral y) (interval [(a,b)])
[INTERIOR_SUBSET_UNION_INTERVALS] Theorem
⊢ ∀s i j.
(∃a b. i = interval [(a,b)]) ∧ (∃c d. j = interval [(c,d)]) ∧
interior j ≠ ∅ ∧ i ⊆ j ∪ s ∧ interior i ∩ interior j = ∅ ⇒
interior i ⊆ interior s
[INTERVAL_BISECTION] Theorem
⊢ ∀P. P ∅ ∧
(∀s t. P s ∧ P t ∧ interior s ∩ interior t = ∅ ⇒ P (s ∪ t)) ⇒
∀a b.
¬P (interval [(a,b)]) ⇒
∃x. x ∈ interval [(a,b)] ∧
∀e. 0 < e ⇒
∃c d.
x ∈ interval [(c,d)] ∧
interval [(c,d)] ⊆ ball (x,e) ∧
interval [(c,d)] ⊆ interval [(a,b)] ∧
¬P (interval [(c,d)])
[INTERVAL_BISECTION_STEP] Theorem
⊢ ∀P. P ∅ ∧
(∀s t. P s ∧ P t ∧ interior s ∩ interior t = ∅ ⇒ P (s ∪ t)) ⇒
∀a b.
¬P (interval [(a,b)]) ⇒
∃c d.
¬P (interval [(c,d)]) ∧ a ≤ c ∧ c ≤ d ∧ d ≤ b ∧
2 * (d − c) ≤ b − a
[INTERVAL_DOUBLESPLIT] Theorem
⊢ ∀e a b c.
interval [(a,b)] ∩ {x | abs (x − c) ≤ e} =
interval [(max a (c − e),min b (c + e))]
[INTERVAL_IMAGE_AFFINITY_INTERVAL] Theorem
⊢ ∀a b m c. ∃u v.
IMAGE (λx. m * x + c) (interval [(a,b)]) = interval [(u,v)]
[INTERVAL_SPLIT] Theorem
⊢ ∀a b c.
interval [(a,b)] ∩ {x | x ≤ c} = interval [(a,min b c)] ∧
interval [(a,b)] ∩ {x | x ≥ c} = interval [(max a c,b)]
[INTERVAL_SUBDIVISION] Theorem
⊢ ∀a b c.
c ∈ interval [(a,b)] ⇒
IMAGE
(λs.
interval
[((@f. f = if 1 ∈ s then c else a),
@f. f = if 1 ∈ s then b else c)]) {s | s ⊆ {1 .. 1}} division_of
interval [(a,b)]
[INTER_INTERIOR_BIGUNION_INTERVALS] Theorem
⊢ ∀s f.
FINITE f ∧ open s ∧ (∀t. t ∈ f ⇒ ∃a b. t = interval [(a,b)]) ∧
(∀t. t ∈ f ⇒ s ∩ interior t = ∅) ⇒
s ∩ interior (BIGUNION f) = ∅
[MONOTONE_CONVERGENCE_DECREASING] Theorem
⊢ ∀f g s.
(∀k. f k integrable_on s) ∧ (∀k x. x ∈ s ⇒ f (SUC k) x ≤ f k x) ∧
(∀x. x ∈ s ⇒ ((λk. f k x) ⟶ g x) sequentially) ∧
bounded {integral s (f k) | k ∈ 𝕌(:num)} ⇒
g integrable_on s ∧
((λk. integral s (f k)) ⟶ integral s g) sequentially
[MONOTONE_CONVERGENCE_DECREASING_AE] Theorem
⊢ ∀f g s t.
(∀k. f k integrable_on s) ∧ negligible t ∧
(∀k x. x ∈ s DIFF t ⇒ f (SUC k) x ≤ f k x) ∧
(∀x. x ∈ s DIFF t ⇒ ((λk. f k x) ⟶ g x) sequentially) ∧
bounded {integral s (f k) | k ∈ 𝕌(:num)} ⇒
g integrable_on s ∧
((λk. integral s (f k)) ⟶ integral s g) sequentially
[MONOTONE_CONVERGENCE_INCREASING] Theorem
⊢ ∀f g s.
(∀k. f k integrable_on s) ∧ (∀k x. x ∈ s ⇒ f k x ≤ f (SUC k) x) ∧
(∀x. x ∈ s ⇒ ((λk. f k x) ⟶ g x) sequentially) ∧
bounded {integral s (f k) | k ∈ 𝕌(:num)} ⇒
g integrable_on s ∧
((λk. integral s (f k)) ⟶ integral s g) sequentially
[MONOTONE_CONVERGENCE_INCREASING_AE] Theorem
⊢ ∀f g s t.
(∀k. f k integrable_on s) ∧ negligible t ∧
(∀k x. x ∈ s DIFF t ⇒ f k x ≤ f (SUC k) x) ∧
(∀x. x ∈ s DIFF t ⇒ ((λk. f k x) ⟶ g x) sequentially) ∧
bounded {integral s (f k) | k ∈ 𝕌(:num)} ⇒
g integrable_on s ∧
((λk. integral s (f k)) ⟶ integral s g) sequentially
[MONOTONE_CONVERGENCE_INTERVAL] Theorem
⊢ ∀f g a b.
(∀k. f k integrable_on interval [(a,b)]) ∧
(∀k x. x ∈ interval [(a,b)] ⇒ f k x ≤ f (SUC k) x) ∧
(∀x. x ∈ interval [(a,b)] ⇒ ((λk. f k x) ⟶ g x) sequentially) ∧
bounded {integral (interval [(a,b)]) (f k) | k ∈ 𝕌(:num)} ⇒
g integrable_on interval [(a,b)] ∧
((λk. integral (interval [(a,b)]) (f k)) ⟶
integral (interval [(a,b)]) g) sequentially
[NEGLIGIBLE] Theorem
⊢ ∀s. negligible s ⇔ ∀t. (indicator s has_integral 0) t
[NEGLIGIBLE_BIGUNION] Theorem
⊢ ∀s. FINITE s ∧ (∀t. t ∈ s ⇒ negligible t) ⇒ negligible (BIGUNION s)
[NEGLIGIBLE_BOUNDED_SUBSETS] Theorem
⊢ ∀s. negligible s ⇔ ∀t. bounded t ∧ t ⊆ s ⇒ negligible t
[NEGLIGIBLE_COUNTABLE] Theorem
⊢ ∀s. countable s ⇒ negligible s
[NEGLIGIBLE_COUNTABLE_BIGUNION] Theorem
⊢ ∀s. (∀n. negligible (s n)) ⇒
negligible (BIGUNION {s n | n ∈ 𝕌(:num)})
[NEGLIGIBLE_DIFF] Theorem
⊢ ∀s t. negligible s ⇒ negligible (s DIFF t)
[NEGLIGIBLE_EMPTY] Theorem
⊢ negligible ∅
[NEGLIGIBLE_FINITE] Theorem
⊢ ∀s. FINITE s ⇒ negligible s
[NEGLIGIBLE_FRONTIER_INTERVAL] Theorem
⊢ ∀a b. negligible (interval [(a,b)] DIFF interval (a,b))
[NEGLIGIBLE_INSERT] Theorem
⊢ ∀a s. negligible (a INSERT s) ⇔ negligible s
[NEGLIGIBLE_INTER] Theorem
⊢ ∀s t. negligible s ∨ negligible t ⇒ negligible (s ∩ t)
[NEGLIGIBLE_ON_COUNTABLE_INTERVALS] Theorem
⊢ ∀s. negligible s ⇔ ∀n. negligible (s ∩ interval [(-n,n)])
[NEGLIGIBLE_ON_INTERVALS] Theorem
⊢ ∀s. negligible s ⇔ ∀a b. negligible (s ∩ interval [(a,b)])
[NEGLIGIBLE_ON_UNIV] Theorem
⊢ ∀s. negligible s ⇔ (indicator s has_integral 0) 𝕌(:real)
[NEGLIGIBLE_SING] Theorem
⊢ ∀a. negligible {a}
[NEGLIGIBLE_STANDARD_HYPERPLANE] Theorem
⊢ ∀c. negligible {x | x = c}
[NEGLIGIBLE_SUBSET] Theorem
⊢ ∀s t. negligible s ∧ t ⊆ s ⇒ negligible t
[NEGLIGIBLE_UNION] Theorem
⊢ ∀s t. negligible s ∧ negligible t ⇒ negligible (s ∪ t)
[NEGLIGIBLE_UNION_EQ] Theorem
⊢ ∀s t. negligible (s ∪ t) ⇔ negligible s ∧ negligible t
[NONNEGATIVE_ABSOLUTELY_INTEGRABLE] Theorem
⊢ ∀f s.
(∀x i. x ∈ s ⇒ 0 ≤ f x) ∧ f integrable_on s ⇒
f absolutely_integrable_on s
[NONNEGATIVE_ABSOLUTELY_INTEGRABLE_AE] Theorem
⊢ ∀f s t.
negligible t ∧ (∀x i. x ∈ s DIFF t ⇒ 0 ≤ f x) ∧ f integrable_on s ⇒
f absolutely_integrable_on s
[OPERATIVE_1_LE] Theorem
⊢ ∀op.
monoidal op ⇒
∀f. operative op f ⇔
(∀a b. b ≤ a ⇒ f (interval [(a,b)]) = neutral op) ∧
∀a b c.
a ≤ c ∧ c ≤ b ⇒
op (f (interval [(a,c)])) (f (interval [(c,b)])) =
f (interval [(a,b)])
[OPERATIVE_1_LT] Theorem
⊢ ∀op.
monoidal op ⇒
∀f. operative op f ⇔
(∀a b. b ≤ a ⇒ f (interval [(a,b)]) = neutral op) ∧
∀a b c.
a < c ∧ c < b ⇒
op (f (interval [(a,c)])) (f (interval [(c,b)])) =
f (interval [(a,b)])
[OPERATIVE_APPROXIMABLE] Theorem
⊢ ∀f e.
0 ≤ e ⇒
operative $/\
(λi. ∃g. (∀x. x ∈ i ⇒ abs (f x − g x) ≤ e) ∧ g integrable_on i)
[OPERATIVE_CONTENT] Theorem
⊢ operative $+ content
[OPERATIVE_DIVISION] Theorem
⊢ ∀op d a b f.
monoidal op ∧ operative op f ∧ d division_of interval [(a,b)] ⇒
iterate op d f = f (interval [(a,b)])
[OPERATIVE_DIVISION_AND] Theorem
⊢ ∀P d a b.
operative $/\ P ∧ d division_of interval [(a,b)] ⇒
((∀i. i ∈ d ⇒ P i) ⇔ P (interval [(a,b)]))
[OPERATIVE_EMPTY] Theorem
⊢ ∀op f. operative op f ⇒ f ∅ = neutral op
[OPERATIVE_FUNCTION_ENDPOINT_DIFF] Theorem
⊢ ∀f. operative $+
(λk. f (interval_upperbound k) − f (interval_lowerbound k))
[OPERATIVE_INTEGRABLE] Theorem
⊢ ∀f. operative $/\ (λi. f integrable_on i)
[OPERATIVE_INTEGRAL] Theorem
⊢ ∀f. operative (lifted $+)
(λi. if f integrable_on i then SOME (integral i f) else NONE)
[OPERATIVE_LIFTED_SETVARIATION] Theorem
⊢ ∀f. operative $+ f ⇒
operative (lifted $+)
(λi.
if f has_bounded_setvariation_on i then
SOME (set_variation i f)
else NONE)
[OPERATIVE_LIFTED_VECTOR_VARIATION] Theorem
⊢ ∀f. operative (lifted $+)
(λi.
if f has_bounded_variation_on i then
SOME (vector_variation i f)
else NONE)
[OPERATIVE_REAL_FUNCTION_ENDPOINT_DIFF] Theorem
⊢ ∀f. operative $+
(λk. f (interval_upperbound k) − f (interval_lowerbound k))
[OPERATIVE_TAGGED_DIVISION] Theorem
⊢ ∀op d a b f.
monoidal op ∧ operative op f ∧
d tagged_division_of interval [(a,b)] ⇒
iterate op d (λ(x,l). f l) = f (interval [(a,b)])
[OPERATIVE_TRIVIAL] Theorem
⊢ ∀op f a b.
operative op f ∧ content (interval [(a,b)]) = 0 ⇒
f (interval [(a,b)]) = neutral op
[PARTIAL_DIVISION_EXTEND] Theorem
⊢ ∀p q s t.
p division_of s ∧ q division_of t ∧ s ⊆ t ⇒
∃r. p ⊆ r ∧ r division_of t
[PARTIAL_DIVISION_EXTEND_1] Theorem
⊢ ∀a b c d.
interval [(c,d)] ⊆ interval [(a,b)] ∧ interval [(c,d)] ≠ ∅ ⇒
∃p. p division_of interval [(a,b)] ∧ interval [(c,d)] ∈ p
[PARTIAL_DIVISION_EXTEND_INTERVAL] Theorem
⊢ ∀p a b.
p division_of BIGUNION p ∧ BIGUNION p ⊆ interval [(a,b)] ⇒
∃q. p ⊆ q ∧ q division_of interval [(a,b)]
[PARTIAL_DIVISION_OF_TAGGED_DIVISION] Theorem
⊢ ∀s i.
s tagged_partial_division_of i ⇒
IMAGE SND s division_of BIGUNION (IMAGE SND s)
[PROPERTY_EMPTY_INTERVAL] Theorem
⊢ ∀P. (∀a b. content (interval [(a,b)]) = 0 ⇒ P (interval [(a,b)])) ⇒
P ∅
[REAL_MUL_POS_LT] Theorem
⊢ ∀x y. 0 < x * y ⇔ 0 < x ∧ 0 < y ∨ x < 0 ∧ y < 0
[RSUM_BOUND] Theorem
⊢ ∀p a b f e.
p tagged_division_of interval [(a,b)] ∧
(∀x. x ∈ interval [(a,b)] ⇒ abs (f x) ≤ e) ⇒
abs (sum p (λ(x,k). content k * f x)) ≤
e * content (interval [(a,b)])
[RSUM_COMPONENT_LE] Theorem
⊢ ∀p a b f g.
p tagged_division_of interval [(a,b)] ∧
(∀x. x ∈ interval [(a,b)] ⇒ f x ≤ g x) ⇒
sum p (λ(x,k). content k * f x) ≤ sum p (λ(x,k). content k * g x)
[RSUM_DIFF_BOUND] Theorem
⊢ ∀e p a b f g.
p tagged_division_of interval [(a,b)] ∧
(∀x. x ∈ interval [(a,b)] ⇒ abs (f x − g x) ≤ e) ⇒
abs
(sum p (λ(x,k). content k * f x) −
sum p (λ(x,k). content k * g x)) ≤
e * content (interval [(a,b)])
[SECOND_MEAN_VALUE_THEOREM] Theorem
⊢ ∀f g a b.
interval [(a,b)] ≠ ∅ ∧ f integrable_on interval [(a,b)] ∧
(∀x y.
x ∈ interval [(a,b)] ∧ y ∈ interval [(a,b)] ∧ x ≤ y ⇒
g x ≤ g y) ⇒
∃c. c ∈ interval [(a,b)] ∧
integral (interval [(a,b)]) (λx. g x * f x) =
g a * integral (interval [(a,c)]) f +
g b * integral (interval [(c,b)]) f
[SECOND_MEAN_VALUE_THEOREM_BONNET] Theorem
⊢ ∀f g a b.
interval [(a,b)] ≠ ∅ ∧ f integrable_on interval [(a,b)] ∧
(∀x. x ∈ interval [(a,b)] ⇒ 0 ≤ g x) ∧
(∀x y.
x ∈ interval [(a,b)] ∧ y ∈ interval [(a,b)] ∧ x ≤ y ⇒
g x ≤ g y) ⇒
∃c. c ∈ interval [(a,b)] ∧
integral (interval [(a,b)]) (λx. g x * f x) =
g b * integral (interval [(c,b)]) f
[SECOND_MEAN_VALUE_THEOREM_BONNET_FULL] Theorem
⊢ ∀f g a b.
interval [(a,b)] ≠ ∅ ∧ f integrable_on interval [(a,b)] ∧
(∀x. x ∈ interval [(a,b)] ⇒ 0 ≤ g x) ∧
(∀x y.
x ∈ interval [(a,b)] ∧ y ∈ interval [(a,b)] ∧ x ≤ y ⇒
g x ≤ g y) ⇒
∃c. c ∈ interval [(a,b)] ∧
((λx. g x * f x) has_integral
g b * integral (interval [(c,b)]) f) (interval [(a,b)])
[SECOND_MEAN_VALUE_THEOREM_FULL] Theorem
⊢ ∀f g a b.
interval [(a,b)] ≠ ∅ ∧ f integrable_on interval [(a,b)] ∧
(∀x y.
x ∈ interval [(a,b)] ∧ y ∈ interval [(a,b)] ∧ x ≤ y ⇒
g x ≤ g y) ⇒
∃c. c ∈ interval [(a,b)] ∧
((λx. g x * f x) has_integral
g a * integral (interval [(a,c)]) f +
g b * integral (interval [(c,b)]) f) (interval [(a,b)])
[SECOND_MEAN_VALUE_THEOREM_GEN] Theorem
⊢ ∀f g a b u v.
interval [(a,b)] ≠ ∅ ∧ f integrable_on interval [(a,b)] ∧
(∀x. x ∈ interval (a,b) ⇒ u ≤ g x ∧ g x ≤ v) ∧
(∀x y.
x ∈ interval [(a,b)] ∧ y ∈ interval [(a,b)] ∧ x ≤ y ⇒
g x ≤ g y) ⇒
∃c. c ∈ interval [(a,b)] ∧
integral (interval [(a,b)]) (λx. g x * f x) =
u * integral (interval [(a,c)]) f +
v * integral (interval [(c,b)]) f
[SECOND_MEAN_VALUE_THEOREM_GEN_FULL] Theorem
⊢ ∀f g a b u v.
interval [(a,b)] ≠ ∅ ∧ f integrable_on interval [(a,b)] ∧
(∀x. x ∈ interval (a,b) ⇒ u ≤ g x ∧ g x ≤ v) ∧
(∀x y.
x ∈ interval [(a,b)] ∧ y ∈ interval [(a,b)] ∧ x ≤ y ⇒
g x ≤ g y) ⇒
∃c. c ∈ interval [(a,b)] ∧
((λx. g x * f x) has_integral
u * integral (interval [(a,c)]) f +
v * integral (interval [(c,b)]) f) (interval [(a,b)])
[SETVARIATION_EQUAL_LEMMA] Theorem
⊢ ∀mf ms ms'.
(∀s. ms' (ms s) = s ∧ ms (ms' s) = s) ∧
(∀f a b.
interval [(a,b)] ≠ ∅ ⇒
mf f (ms (interval [(a,b)])) = f (interval [(a,b)]) ∧
∃a' b'.
interval [(a',b')] ≠ ∅ ∧
ms' (interval [(a,b)]) = interval [(a',b')]) ∧
(∀t u. t ⊆ u ⇒ ms t ⊆ ms u ∧ ms' t ⊆ ms' u) ∧
(∀d t.
d division_of t ⇒
IMAGE ms d division_of ms t ∧ IMAGE ms' d division_of ms' t) ⇒
(∀f s.
mf f has_bounded_setvariation_on ms s ⇔
f has_bounded_setvariation_on s) ∧
∀f s. set_variation (ms s) (mf f) = set_variation s f
[SET_VARIATION] Theorem
⊢ ∀f s d t.
f has_bounded_setvariation_on s ∧ d division_of t ∧ t ⊆ s ⇒
sum d (λk. abs (f k)) ≤ set_variation s f
[SET_VARIATION_0] Theorem
⊢ ∀s. set_variation s (λx. 0) = 0
[SET_VARIATION_COMPARISON] Theorem
⊢ ∀f g s.
f has_bounded_setvariation_on s ∧
(∀a b.
interval [(a,b)] ≠ ∅ ∧ interval [(a,b)] ⊆ s ⇒
abs (g (interval [(a,b)])) ≤ abs (f (interval [(a,b)]))) ⇒
set_variation s g ≤ set_variation s f
[SET_VARIATION_ELEMENTARY_LEMMA] Theorem
⊢ ∀f s b.
(∃d. d division_of s) ⇒
((∀d t. d division_of t ∧ t ⊆ s ⇒ sum d (λk. abs (f k)) ≤ b) ⇔
∀d. d division_of s ⇒ sum d (λk. abs (f k)) ≤ b)
[SET_VARIATION_EQ] Theorem
⊢ ∀f g s.
(∀a b.
interval [(a,b)] ≠ ∅ ∧ interval [(a,b)] ⊆ s ⇒
f (interval [(a,b)]) = g (interval [(a,b)])) ⇒
set_variation s f = set_variation s g
[SET_VARIATION_GE_FUNCTION] Theorem
⊢ ∀f s a b.
f has_bounded_setvariation_on s ∧ interval [(a,b)] ⊆ s ∧
interval [(a,b)] ≠ ∅ ⇒
abs (f (interval [(a,b)])) ≤ set_variation s f
[SET_VARIATION_LBOUND] Theorem
⊢ ∀f s B.
f has_bounded_setvariation_on s ∧
(∃d t. d division_of t ∧ t ⊆ s ∧ B ≤ sum d (λk. abs (f k))) ⇒
B ≤ set_variation s f
[SET_VARIATION_LBOUND_ON_INTERVAL] Theorem
⊢ ∀f a b B.
f has_bounded_setvariation_on interval [(a,b)] ∧
(∃d. d division_of interval [(a,b)] ∧ B ≤ sum d (λk. abs (f k))) ⇒
B ≤ set_variation (interval [(a,b)]) f
[SET_VARIATION_MONOTONE] Theorem
⊢ ∀f s t.
f has_bounded_setvariation_on s ∧ t ⊆ s ⇒
set_variation t f ≤ set_variation s f
[SET_VARIATION_ON_DIVISION] Theorem
⊢ ∀f a b d.
operative $+ f ∧ d division_of interval [(a,b)] ∧
f has_bounded_setvariation_on interval [(a,b)] ⇒
sum d (λk. set_variation k f) =
set_variation (interval [(a,b)]) f
[SET_VARIATION_ON_ELEMENTARY] Theorem
⊢ ∀f s.
(∃d. d division_of s) ⇒
set_variation s f = sup {sum d (λk. abs (f k)) | d division_of s}
[SET_VARIATION_ON_INTERVAL] Theorem
⊢ ∀f a b.
set_variation (interval [(a,b)]) f =
sup {sum d (λk. abs (f k)) | d division_of interval [(a,b)]}
[SET_VARIATION_ON_NULL] Theorem
⊢ ∀f s.
(∀a b. content (interval [(a,b)]) = 0 ⇒ f (interval [(a,b)]) = 0) ∧
content s = 0 ∧ bounded s ⇒
set_variation s f = 0
[SET_VARIATION_POS_LE] Theorem
⊢ ∀f s. f has_bounded_setvariation_on s ⇒ 0 ≤ set_variation s f
[SET_VARIATION_REFLECT2] Theorem
⊢ ∀f s.
set_variation (IMAGE (λx. -x) s) (λk. f (IMAGE (λx. -x) k)) =
set_variation s f
[SET_VARIATION_SUM_LE] Theorem
⊢ ∀f s k.
FINITE k ∧ (∀i. i ∈ k ⇒ f i has_bounded_setvariation_on s) ⇒
set_variation s (λx. sum k (λi. f i x)) ≤
sum k (λi. set_variation s (f i))
[SET_VARIATION_TRANSLATION2] Theorem
⊢ ∀a f s.
set_variation (IMAGE (λx. -a + x) s)
(λk. f (IMAGE (λx. a + x) k)) =
set_variation s f
[SET_VARIATION_TRIANGLE] Theorem
⊢ ∀f g s.
f has_bounded_setvariation_on s ∧ g has_bounded_setvariation_on s ⇒
set_variation s (λx. f x + g x) ≤
set_variation s f + set_variation s g
[SET_VARIATION_UBOUND] Theorem
⊢ ∀f s B.
f has_bounded_setvariation_on s ∧
(∀d t. d division_of t ∧ t ⊆ s ⇒ sum d (λk. abs (f k)) ≤ B) ⇒
set_variation s f ≤ B
[SET_VARIATION_UBOUND_ON_INTERVAL] Theorem
⊢ ∀f a b B.
f has_bounded_setvariation_on interval [(a,b)] ∧
(∀d. d division_of interval [(a,b)] ⇒ sum d (λk. abs (f k)) ≤ B) ⇒
set_variation (interval [(a,b)]) f ≤ B
[SET_VARIATION_WORKS_ON_INTERVAL] Theorem
⊢ ∀f a b d.
f has_bounded_setvariation_on interval [(a,b)] ∧
d division_of interval [(a,b)] ⇒
sum d (λk. abs (f k)) ≤ set_variation (interval [(a,b)]) f
[SUBADDITIVE_CONTENT_DIVISION] Theorem
⊢ ∀d s a b.
d division_of s ∧ s ⊆ interval [(a,b)] ⇒
sum d content ≤ content (interval [(a,b)])
[SUM_ABS_ALLSUBSETS_BOUND] Theorem
⊢ ∀f p e.
FINITE p ∧ (∀q. q ⊆ p ⇒ abs (sum q f) ≤ e) ⇒
sum p (λx. abs (f x)) ≤ 2 * 1 * e
[SUM_CONTENT_AREA_OVER_THIN_DIVISION] Theorem
⊢ ∀d a b s c.
d division_of s ∧ s ⊆ interval [(a,b)] ∧ a ≤ c ∧ c ≤ b ∧
(∀k. k ∈ d ⇒ k ∩ {x | x = c} ≠ ∅) ⇒
(b − a) *
sum d
(λk.
content k /
(interval_upperbound k − interval_lowerbound k)) ≤
2 * content (interval [(a,b)])
[SUM_CONTENT_NULL] Theorem
⊢ ∀f a b p.
content (interval [(a,b)]) = 0 ∧
p tagged_division_of interval [(a,b)] ⇒
sum p (λ(x,k). content k * f x) = 0
[SUM_NONZERO_IMAGE_LEMMA] Theorem
⊢ ∀s f g a.
FINITE s ∧ g a = 0 ∧
(∀x y. x ∈ s ∧ y ∈ s ∧ f x = f y ∧ x ≠ y ⇒ g (f x) = 0) ⇒
sum {f x | x | x ∈ s ∧ f x ≠ a} g = sum s (g ∘ f)
[SUM_OVER_TAGGED_DIVISION_LEMMA] Theorem
⊢ ∀d p i.
p tagged_division_of i ∧
(∀u v.
interval [(u,v)] ≠ ∅ ∧ content (interval [(u,v)]) = 0 ⇒
d (interval [(u,v)]) = 0) ⇒
sum p (λ(x,k). d k) = sum (IMAGE SND p) d
[SUM_OVER_TAGGED_PARTIAL_DIVISION_LEMMA] Theorem
⊢ ∀d p i.
p tagged_partial_division_of i ∧
(∀u v.
interval [(u,v)] ≠ ∅ ∧ content (interval [(u,v)]) = 0 ⇒
d (interval [(u,v)]) = 0) ⇒
sum p (λ(x,k). d k) = sum (IMAGE SND p) d
[TAGGED_DIVISION_BIGUNION] Theorem
⊢ ∀iset pfn.
FINITE iset ∧ (∀i. i ∈ iset ⇒ pfn i tagged_division_of i) ∧
(∀i1 i2.
i1 ∈ iset ∧ i2 ∈ iset ∧ i1 ≠ i2 ⇒
interior i1 ∩ interior i2 = ∅) ⇒
BIGUNION (IMAGE pfn iset) tagged_division_of BIGUNION iset
[TAGGED_DIVISION_BIGUNION_EXISTS] Theorem
⊢ ∀d iset i.
FINITE iset ∧
(∀i. i ∈ iset ⇒ ∃p. p tagged_division_of i ∧ d FINE p) ∧
(∀i1 i2.
i1 ∈ iset ∧ i2 ∈ iset ∧ i1 ≠ i2 ⇒
interior i1 ∩ interior i2 = ∅) ∧ BIGUNION iset = i ⇒
∃p. p tagged_division_of i ∧ d FINE p
[TAGGED_DIVISION_FINER] Theorem
⊢ ∀p a b d.
p tagged_division_of interval [(a,b)] ∧ gauge d ⇒
∃q. q tagged_division_of interval [(a,b)] ∧ d FINE q ∧
∀x k. (x,k) ∈ p ∧ k ⊆ d x ⇒ (x,k) ∈ q
[TAGGED_DIVISION_OF] Theorem
⊢ ∀s i.
s tagged_division_of i ⇔
FINITE s ∧
(∀x k. (x,k) ∈ s ⇒ x ∈ k ∧ k ⊆ i ∧ ∃a b. k = interval [(a,b)]) ∧
(∀x1 k1 x2 k2.
(x1,k1) ∈ s ∧ (x2,k2) ∈ s ∧ (x1,k1) ≠ (x2,k2) ⇒
interior k1 ∩ interior k2 = ∅) ∧
BIGUNION {k | (∃x. (x,k) ∈ s)} = i
[TAGGED_DIVISION_OF_ALT] Theorem
⊢ ∀p s.
p tagged_division_of s ⇔
p tagged_partial_division_of s ∧
∀x. x ∈ s ⇒ ∃t k. (t,k) ∈ p ∧ x ∈ k
[TAGGED_DIVISION_OF_ANOTHER] Theorem
⊢ ∀p s s'.
p tagged_partial_division_of s' ∧ (∀t k. (t,k) ∈ p ⇒ k ⊆ s) ∧
(∀x. x ∈ s ⇒ ∃t k. (t,k) ∈ p ∧ x ∈ k) ⇒
p tagged_division_of s
[TAGGED_DIVISION_OF_EMPTY] Theorem
⊢ ∅ tagged_division_of ∅
[TAGGED_DIVISION_OF_FINITE] Theorem
⊢ ∀s i. s tagged_division_of i ⇒ FINITE s
[TAGGED_DIVISION_OF_NONTRIVIAL] Theorem
⊢ ∀s a b.
s tagged_division_of interval [(a,b)] ∧
content (interval [(a,b)]) ≠ 0 ⇒
{(x,k) | (x,k) ∈ s ∧ content k ≠ 0} tagged_division_of
interval [(a,b)]
[TAGGED_DIVISION_OF_SELF] Theorem
⊢ ∀x a b.
x ∈ interval [(a,b)] ⇒
{(x,interval [(a,b)])} tagged_division_of interval [(a,b)]
[TAGGED_DIVISION_OF_TRIVIAL] Theorem
⊢ ∀p. p tagged_division_of ∅ ⇔ p = ∅
[TAGGED_DIVISION_OF_UNION_SELF] Theorem
⊢ ∀p s.
p tagged_division_of s ⇒
p tagged_division_of BIGUNION (IMAGE SND p)
[TAGGED_DIVISION_SPLIT_LEFT_INJ] Theorem
⊢ ∀d i x1 k1 x2 k2 c.
d tagged_division_of i ∧ (x1,k1) ∈ d ∧ (x2,k2) ∈ d ∧ k1 ≠ k2 ∧
k1 ∩ {x | x ≤ c} = k2 ∩ {x | x ≤ c} ⇒
content (k1 ∩ {x | x ≤ c}) = 0
[TAGGED_DIVISION_SPLIT_RIGHT_INJ] Theorem
⊢ ∀d i x1 k1 x2 k2 c.
d tagged_division_of i ∧ (x1,k1) ∈ d ∧ (x2,k2) ∈ d ∧ k1 ≠ k2 ∧
k1 ∩ {x | x ≥ c} = k2 ∩ {x | x ≥ c} ⇒
content (k1 ∩ {x | x ≥ c}) = 0
[TAGGED_DIVISION_UNION] Theorem
⊢ ∀s1 s2 p1 p2.
p1 tagged_division_of s1 ∧ p2 tagged_division_of s2 ∧
interior s1 ∩ interior s2 = ∅ ⇒
p1 ∪ p2 tagged_division_of s1 ∪ s2
[TAGGED_DIVISION_UNION_IMAGE_SND] Theorem
⊢ ∀p s. p tagged_division_of s ⇒ s = BIGUNION (IMAGE SND p)
[TAGGED_DIVISION_UNION_INTERVAL] Theorem
⊢ ∀a b p1 p2 c.
p1 tagged_division_of interval [(a,b)] ∩ {x | x ≤ c} ∧
p2 tagged_division_of interval [(a,b)] ∩ {x | x ≥ c} ⇒
p1 ∪ p2 tagged_division_of interval [(a,b)]
[TAGGED_PARTIAL_DIVISION_COMMON_POINT_BOUND] Theorem
⊢ ∀p s y.
p tagged_partial_division_of s ⇒
CARD {(x,k) | (x,k) ∈ p ∧ y ∈ k ∧ content k ≠ 0} ≤ 2 ** 1
[TAGGED_PARTIAL_DIVISION_COMMON_TAGS] Theorem
⊢ ∀p s x.
p tagged_partial_division_of s ⇒
CARD {(x,k) | k | (x,k) ∈ p ∧ content k ≠ 0} ≤ 2 ** 1
[TAGGED_PARTIAL_DIVISION_OF_SUBSET] Theorem
⊢ ∀p s t.
p tagged_partial_division_of s ∧ s ⊆ t ⇒
p tagged_partial_division_of t
[TAGGED_PARTIAL_DIVISION_OF_TRIVIAL] Theorem
⊢ ∀p. p tagged_partial_division_of ∅ ⇔ p = ∅
[TAGGED_PARTIAL_DIVISION_OF_UNION_SELF] Theorem
⊢ ∀p s.
p tagged_partial_division_of s ⇒
p tagged_division_of BIGUNION (IMAGE SND p)
[TAGGED_PARTIAL_DIVISION_SUBSET] Theorem
⊢ ∀s t i.
s tagged_partial_division_of i ∧ t ⊆ s ⇒
t tagged_partial_division_of i
[TAG_IN_INTERVAL] Theorem
⊢ ∀p i k. p tagged_division_of i ∧ (x,k) ∈ p ⇒ x ∈ i
[VARIATION_EQUAL_LEMMA] Theorem
⊢ ∀ms ms'.
(∀s. ms' (ms s) = s ∧ ms (ms' s) = s) ∧
(∀d t.
d division_of t ⇒
IMAGE (IMAGE ms) d division_of IMAGE ms t ∧
IMAGE (IMAGE ms') d division_of IMAGE ms' t) ∧
(∀a b.
interval [(a,b)] ≠ ∅ ⇒
IMAGE ms' (interval [(a,b)]) = interval [(ms' a,ms' b)] ∨
IMAGE ms' (interval [(a,b)]) = interval [(ms' b,ms' a)]) ⇒
(∀f s.
(λx. f (ms' x)) has_bounded_variation_on IMAGE ms s ⇔
f has_bounded_variation_on s) ∧
∀f s.
vector_variation (IMAGE ms s) (λx. f (ms' x)) =
vector_variation s f
[VECTOR_VARIATION_ABS] Theorem
⊢ ∀f s.
(λx. f x) has_bounded_variation_on s ⇒
vector_variation s (λx. abs (f x)) ≤ vector_variation s (λx. f x)
[VECTOR_VARIATION_AFFINITY] Theorem
⊢ ∀m c f s.
vector_variation s (λx. f (m * x + c)) =
if m = 0 then 0 else vector_variation (IMAGE (λx. m * x + c) s) f
[VECTOR_VARIATION_AFFINITY2] Theorem
⊢ ∀m c f s.
vector_variation (IMAGE (λx. m⁻¹ * x + -(m⁻¹ * c)) s)
(λx. f (m * x + c)) =
if m = 0 then 0 else vector_variation s f
[VECTOR_VARIATION_COMBINE] Theorem
⊢ ∀f a b c.
a ≤ c ∧ c ≤ b ∧ f has_bounded_variation_on interval [(a,b)] ⇒
vector_variation (interval [(a,c)]) f +
vector_variation (interval [(c,b)]) f =
vector_variation (interval [(a,b)]) f
[VECTOR_VARIATION_COMPARISON] Theorem
⊢ ∀f g s.
f has_bounded_variation_on s ∧
(∀x y. x ∈ s ∧ y ∈ s ∧ x < y ⇒ dist (g x,g y) ≤ dist (f x,f y)) ⇒
vector_variation s g ≤ vector_variation s f
[VECTOR_VARIATION_CONST] Theorem
⊢ ∀s c. vector_variation s (λx. c) = 0
[VECTOR_VARIATION_CONST_EQ] Theorem
⊢ ∀f s.
is_interval s ∧ f has_bounded_variation_on s ⇒
(vector_variation s f = 0 ⇔ ∃c. ∀x. x ∈ s ⇒ f x = c)
[VECTOR_VARIATION_CONTINUOUS] Theorem
⊢ ∀f a b c.
f has_bounded_variation_on interval [(a,b)] ∧
c ∈ interval [(a,b)] ⇒
((λx. vector_variation (interval [(a,x)]) f) continuous
(at c within interval [(a,b)]) ⇔
f continuous (at c within interval [(a,b)]))
[VECTOR_VARIATION_CONTINUOUS_LEFT] Theorem
⊢ ∀f a b c.
f has_bounded_variation_on interval [(a,b)] ∧
c ∈ interval [(a,b)] ⇒
((λx. vector_variation (interval [(a,x)]) f) continuous
(at c within interval [(a,c)]) ⇔
f continuous (at c within interval [(a,c)]))
[VECTOR_VARIATION_CONTINUOUS_RIGHT] Theorem
⊢ ∀f a b c.
f has_bounded_variation_on interval [(a,b)] ∧
c ∈ interval [(a,b)] ⇒
((λx. vector_variation (interval [(a,x)]) f) continuous
(at c within interval [(c,b)]) ⇔
f continuous (at c within interval [(c,b)]))
[VECTOR_VARIATION_EQ] Theorem
⊢ ∀f g s.
(∀x. x ∈ s ⇒ f x = g x) ⇒
vector_variation s f = vector_variation s g
[VECTOR_VARIATION_GE_ABS_FUNCTION] Theorem
⊢ ∀f s a b.
f has_bounded_variation_on s ∧ segment [(a,b)] ⊆ s ⇒
abs (f b − f a) ≤ vector_variation s f
[VECTOR_VARIATION_GE_FUNCTION] Theorem
⊢ ∀f s a b.
f has_bounded_variation_on s ∧ segment [(a,b)] ⊆ s ⇒
f b − f a ≤ vector_variation s f
[VECTOR_VARIATION_MINUS_FUNCTION_MONOTONE] Theorem
⊢ ∀f a b c d.
f has_bounded_variation_on interval [(a,b)] ∧
interval [(c,d)] ⊆ interval [(a,b)] ∧ interval [(c,d)] ≠ ∅ ⇒
vector_variation (interval [(c,d)]) f − (f d − f c) ≤
vector_variation (interval [(a,b)]) f − (f b − f a)
[VECTOR_VARIATION_MONOTONE] Theorem
⊢ ∀f s t.
f has_bounded_variation_on s ∧ t ⊆ s ⇒
vector_variation t f ≤ vector_variation s f
[VECTOR_VARIATION_NEG] Theorem
⊢ ∀f s. vector_variation s (λx. -f x) = vector_variation s f
[VECTOR_VARIATION_ON_DIVISION] Theorem
⊢ ∀f a b d.
d division_of interval [(a,b)] ∧
f has_bounded_variation_on interval [(a,b)] ⇒
sum d (λk. vector_variation k f) =
vector_variation (interval [(a,b)]) f
[VECTOR_VARIATION_ON_NULL] Theorem
⊢ ∀f s. content s = 0 ∧ bounded s ⇒ vector_variation s f = 0
[VECTOR_VARIATION_POS_LE] Theorem
⊢ ∀f s. f has_bounded_variation_on s ⇒ 0 ≤ vector_variation s f
[VECTOR_VARIATION_REFLECT] Theorem
⊢ ∀f s.
vector_variation s (λx. f (-x)) =
vector_variation (IMAGE (λx. -x) s) f
[VECTOR_VARIATION_REFLECT2] Theorem
⊢ ∀f s.
vector_variation (IMAGE (λx. -x) s) (λx. f (-x)) =
vector_variation s f
[VECTOR_VARIATION_REFLECT_INTERVAL] Theorem
⊢ ∀f u v.
vector_variation (interval [(u,v)]) (λx. f (-x)) =
vector_variation (interval [(-v,-u)]) f
[VECTOR_VARIATION_TRANSLATION] Theorem
⊢ ∀a f s.
vector_variation s (λx. f (a + x)) =
vector_variation (IMAGE (λx. a + x) s) f
[VECTOR_VARIATION_TRANSLATION2] Theorem
⊢ ∀a f s.
vector_variation (IMAGE (λx. -a + x) s) (λx. f (a + x)) =
vector_variation s f
[VECTOR_VARIATION_TRANSLATION_INTERVAL] Theorem
⊢ ∀a f u v.
vector_variation (interval [(u,v)]) (λx. f (a + x)) =
vector_variation (interval [(a + u,a + v)]) f
[VECTOR_VARIATION_TRIANGLE] Theorem
⊢ ∀f g s.
f has_bounded_variation_on s ∧ g has_bounded_variation_on s ⇒
vector_variation s (λx. f x + g x) ≤
vector_variation s f + vector_variation s g
[has_integral] Theorem
⊢ ∀f y a b.
(f has_integral y) (interval [(a,b)]) ⇔
∀e. 0 < e ⇒
∃d. gauge d ∧
∀p. p tagged_division_of interval [(a,b)] ∧ d FINE p ⇒
abs (sum p (λ(x,k). content k * f x) − y) < e
[has_integral_alt] Theorem
⊢ ∀f i y.
(f has_integral y) i ⇔
if ∃a b. i = interval [(a,b)] then (f has_integral y) i
else
∀e. 0 < e ⇒
∃B. 0 < B ∧
∀a b.
ball (0,B) ⊆ interval [(a,b)] ⇒
∃z. ((λx. if x ∈ i then f x else 0) has_integral z)
(interval [(a,b)]) ∧ abs (z − y) < e
*)
end
HOL 4, Trindemossen-1