Please see our privacy statement for more information.
lemma series_differentiable_comparison_complex: fixesS::"complex set" assumes S:"open S" and hfd:"⋀nx.x∈S⟹fnfield_differentiable(atx)" and to_g:"⋀x.x∈S⟹∃dh.0<d∧ summable h∧ range h⊆ℝ⇩≥⇩0∧(∀⇩Fnin sequentially.∀y∈ball xd∩S. cmod(fny)≤ cmod (hn))" obtainsgwhere"∀x∈S.((λn.fnx)sumsgx)∧gfield_differentiable(atx)" proof- have hfd':"⋀nx.x∈S⟹(fnhas_field_derivative deriv (fn)x)(atx)" using hfd field_differentiable_derivI byblast have"∃gg'.∀x∈S.((λn.fnx)sumsgx)∧((λn. deriv (fn)x)sumsg'x)∧(ghas_field_derivativeg'x)(atx)" by(metis series_and_derivative_comparison_complex [OF S hfd' to_g]) thenshow?thesis using field_differentiable_def that byblast qed
text‹In particular, a power series is analytic inside circle of convergence.›
definition integral::"('a⇒ real)⇒('a set set *('a set ⇒ real))⇒ real"("∫ _ ∂_"(*<*)[60,61] 110(*>*))where "integrable fM⟹∫f∂M=(THEi.i∈ nnfis (ppf)M)- (THEj.j∈ nnfis (npf)M)"
text‹So the final step is done, the integral defined. The theorems we are already used to prove from the earlier stages are still missing. Only now there are always two properties to be shown: integrability and the value of the integral. Isabelle makes it possible two have both goals in a single theorem, so that the user may derive the statement he desires. Two useful lemmata follow. They help lifting nonnegative function integral sets to integrals proper. Notice how the dominated convergence theorem from above is employed in the latter.›