author immler Wed, 16 Jan 2019 19:34:48 -0500 changeset 69676 56acd449da41 parent 69675 880ab0f27ddf child 69679 a8faf6f15da7
chapters for analysis manual
 src/HOL/Analysis/Analysis.thy file | annotate | diff | comparison | revisions src/HOL/Analysis/Elementary_Metric_Spaces.thy file | annotate | diff | comparison | revisions src/HOL/Analysis/Elementary_Topology.thy file | annotate | diff | comparison | revisions src/HOL/Analysis/L2_Norm.thy file | annotate | diff | comparison | revisions src/HOL/Analysis/Sigma_Algebra.thy file | annotate | diff | comparison | revisions src/HOL/Analysis/Starlike.thy file | annotate | diff | comparison | revisions src/HOL/Analysis/Topology_Euclidean_Space.thy file | annotate | diff | comparison | revisions src/HOL/Analysis/document/root.tex file | annotate | diff | comparison | revisions
```--- a/src/HOL/Analysis/Analysis.thy	Wed Jan 16 18:14:02 2019 -0500
+++ b/src/HOL/Analysis/Analysis.thy	Wed Jan 16 19:34:48 2019 -0500
@@ -1,5 +1,20 @@
theory Analysis
-imports
+  imports
+  (* Linear Algebra *)
+  Convex
+  Determinants
+  (* Topology *)
+  Connected
+  (* Functional Analysis *)
+  Elementary_Normed_Spaces
+  Norm_Arith
+  (* Vector Analysis *)
+  Convex_Euclidean_Space
+  (* Measure and Integration Theory *)
+  Ball_Volume
+  Integral_Test
+  Improper_Integral
+  (* Unsorted *)
Lebesgue_Integral_Substitution
Improper_Integral
Embed_Measure```
```--- a/src/HOL/Analysis/Elementary_Metric_Spaces.thy	Wed Jan 16 18:14:02 2019 -0500
+++ b/src/HOL/Analysis/Elementary_Metric_Spaces.thy	Wed Jan 16 19:34:48 2019 -0500
@@ -4,13 +4,15 @@
Author:     Brian Huffman, Portland State University
*)

-section \<open>Elementary Metric Spaces\<close>
+chapter \<open>Functional Analysis\<close>

theory Elementary_Metric_Spaces
imports
Abstract_Topology_2
begin

+section \<open>Elementary Metric Spaces\<close>
+
subsection \<open>Open and closed balls\<close>

definition%important ball :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set"```
```--- a/src/HOL/Analysis/Elementary_Topology.thy	Wed Jan 16 18:14:02 2019 -0500
+++ b/src/HOL/Analysis/Elementary_Topology.thy	Wed Jan 16 19:34:48 2019 -0500
@@ -4,7 +4,7 @@
Author:     Brian Huffman, Portland State University
*)

-section \<open>Elementary Topology\<close>
+chapter \<open>Topology\<close>

theory Elementary_Topology
imports
@@ -14,6 +14,8 @@
begin

+section \<open>Elementary Topology\<close>
+
subsection \<open>TODO: move?\<close>

lemma open_subopen: "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> S)"```
```--- a/src/HOL/Analysis/L2_Norm.thy	Wed Jan 16 18:14:02 2019 -0500
+++ b/src/HOL/Analysis/L2_Norm.thy	Wed Jan 16 19:34:48 2019 -0500
@@ -2,12 +2,14 @@
Author:     Brian Huffman, Portland State University
*)

-section \<open>L2 Norm\<close>
+chapter \<open>Linear Algebra\<close>

theory L2_Norm
imports Complex_Main
begin

+section \<open>L2 Norm\<close>
+
definition%important L2_set :: "('a \<Rightarrow> real) \<Rightarrow> 'a set \<Rightarrow> real" where
"L2_set f A = sqrt (\<Sum>i\<in>A. (f i)\<^sup>2)"
```
```--- a/src/HOL/Analysis/Sigma_Algebra.thy	Wed Jan 16 18:14:02 2019 -0500
+++ b/src/HOL/Analysis/Sigma_Algebra.thy	Wed Jan 16 19:34:48 2019 -0500
@@ -5,7 +5,7 @@
translated by Lawrence Paulson.
*)

-section \<open>Sigma Algebra\<close>
+chapter \<open>Measure and Integration Theory\<close>

theory Sigma_Algebra
imports
@@ -17,6 +17,9 @@
"HOL-Library.Disjoint_Sets"
begin

+
+section \<open>Sigma Algebra\<close>
+
text \<open>Sigma algebras are an elementary concept in measure
theory. To measure --- that is to integrate --- functions, we first have
to measure sets. Unfortunately, when dealing with a large universe,```
```--- a/src/HOL/Analysis/Starlike.thy	Wed Jan 16 18:14:02 2019 -0500
+++ b/src/HOL/Analysis/Starlike.thy	Wed Jan 16 19:34:48 2019 -0500
@@ -5,13 +5,14 @@
Author:     Armin Heller, TU Muenchen
Author:     Johannes Hoelzl, TU Muenchen
*)
-
-section \<open>Line Segments\<close>
+chapter \<open>Unsorted\<close>

theory Starlike
imports Convex_Euclidean_Space
begin

+section \<open>Line Segments\<close>
+
subsection \<open>Midpoint\<close>

definition%important midpoint :: "'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a"```
```--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Wed Jan 16 18:14:02 2019 -0500
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Wed Jan 16 19:34:48 2019 -0500
@@ -4,7 +4,7 @@
Author:     Brian Huffman, Portland State University
*)

-section \<open>Elementary Topology in Euclidean Space\<close>
+chapter \<open>Vector Analysis\<close>

theory Topology_Euclidean_Space
imports
@@ -13,6 +13,8 @@
Norm_Arith
begin

+section \<open>Elementary Topology in Euclidean Space\<close>
+
lemma euclidean_dist_l2:
fixes x y :: "'a :: euclidean_space"
shows "dist x y = L2_set (\<lambda>i. dist (x \<bullet> i) (y \<bullet> i)) Basis"```
```--- a/src/HOL/Analysis/document/root.tex	Wed Jan 16 18:14:02 2019 -0500
+++ b/src/HOL/Analysis/document/root.tex	Wed Jan 16 19:34:48 2019 -0500
@@ -1,4 +1,4 @@
-\documentclass[11pt,a4paper]{article}
+\documentclass[11pt,a4paper]{book}
\usepackage{graphicx}
\usepackage{isabelle}
\usepackage{isabellesym}```