more antiquotations -- less LaTeX macros;
authorwenzelm
Tue Jan 01 21:47:27 2019 +0100 (4 months ago)
changeset 69566c41954ee87cf
parent 69565 1daf07b65385
child 69570 2f78e0d73a34
more antiquotations -- less LaTeX macros;
src/HOL/Analysis/Ball_Volume.thy
src/HOL/Analysis/Binary_Product_Measure.thy
src/HOL/Analysis/Bochner_Integration.thy
src/HOL/Analysis/Borel_Space.thy
src/HOL/Analysis/Brouwer_Fixpoint.thy
src/HOL/Analysis/Complete_Measure.thy
src/HOL/Analysis/Complex_Transcendental.thy
src/HOL/Analysis/Embed_Measure.thy
src/HOL/Analysis/Extended_Real_Limits.thy
src/HOL/Analysis/Function_Topology.thy
src/HOL/Analysis/Further_Topology.thy
src/HOL/Analysis/Gamma_Function.thy
src/HOL/Analysis/Lipschitz.thy
src/HOL/Analysis/Measure_Space.thy
src/HOL/Analysis/Path_Connected.thy
src/HOL/Analysis/Set_Integral.thy
src/HOL/Analysis/Sigma_Algebra.thy
     1.1 --- a/src/HOL/Analysis/Ball_Volume.thy	Tue Jan 01 20:57:54 2019 +0100
     1.2 +++ b/src/HOL/Analysis/Ball_Volume.thy	Tue Jan 01 21:47:27 2019 +0100
     1.3 @@ -3,7 +3,7 @@
     1.4     Author:   Manuel Eberl, TU M√ľnchen
     1.5  *)
     1.6  
     1.7 -section \<open>The Volume of an $n$-Dimensional Ball\<close>
     1.8 +section \<open>The Volume of an \<open>n\<close>-Dimensional Ball\<close>
     1.9  
    1.10  theory Ball_Volume
    1.11    imports Gamma_Function Lebesgue_Integral_Substitution
    1.12 @@ -25,8 +25,8 @@
    1.13  
    1.14  text \<open>
    1.15    We first need the value of the following integral, which is at the core of
    1.16 -  computing the measure of an $n+1$-dimensional ball in terms of the measure of an 
    1.17 -  $n$-dimensional one.
    1.18 +  computing the measure of an \<open>n + 1\<close>-dimensional ball in terms of the measure of an 
    1.19 +  \<open>n\<close>-dimensional one.
    1.20  \<close>
    1.21  lemma emeasure_cball_aux_integral:
    1.22    "(\<integral>\<^sup>+x. indicator {-1..1} x * sqrt (1 - x\<^sup>2) ^ n \<partial>lborel) = 
     2.1 --- a/src/HOL/Analysis/Binary_Product_Measure.thy	Tue Jan 01 20:57:54 2019 +0100
     2.2 +++ b/src/HOL/Analysis/Binary_Product_Measure.thy	Tue Jan 01 21:47:27 2019 +0100
     2.3 @@ -336,7 +336,7 @@
     2.4      by (simp add: ac_simps)
     2.5  qed
     2.6  
     2.7 -subsection%important \<open>Binary products of $\sigma$-finite emeasure spaces\<close>
     2.8 +subsection%important \<open>Binary products of \<open>\<sigma>\<close>-finite emeasure spaces\<close>
     2.9  
    2.10  locale%important pair_sigma_finite = M1?: sigma_finite_measure M1 + M2?: sigma_finite_measure M2
    2.11    for M1 :: "'a measure" and M2 :: "'b measure"
     3.1 --- a/src/HOL/Analysis/Bochner_Integration.thy	Tue Jan 01 20:57:54 2019 +0100
     3.2 +++ b/src/HOL/Analysis/Bochner_Integration.thy	Tue Jan 01 21:47:27 2019 +0100
     3.3 @@ -2100,7 +2100,7 @@
     3.4    then show ?thesis using Lim_null by auto
     3.5  qed
     3.6  
     3.7 -text \<open>The next lemma asserts that, if a sequence of functions converges in $L^1$, then
     3.8 +text \<open>The next lemma asserts that, if a sequence of functions converges in \<open>L\<^sup>1\<close>, then
     3.9  it admits a subsequence that converges almost everywhere.\<close>
    3.10  
    3.11  lemma%important tendsto_L1_AE_subseq:
     4.1 --- a/src/HOL/Analysis/Borel_Space.thy	Tue Jan 01 20:57:54 2019 +0100
     4.2 +++ b/src/HOL/Analysis/Borel_Space.thy	Tue Jan 01 21:47:27 2019 +0100
     4.3 @@ -2140,7 +2140,7 @@
     4.4    shows "(\<lambda>x. \<bar>f x\<bar> powr p) \<in> borel_measurable M"
     4.5  unfolding powr_def by auto
     4.6  
     4.7 -text \<open>The next one is a variation around \verb+measurable_restrict_space+.\<close>
     4.8 +text \<open>The next one is a variation around \<open>measurable_restrict_space\<close>.\<close>
     4.9  
    4.10  lemma%unimportant measurable_restrict_space3:
    4.11    assumes "f \<in> measurable M N" and
    4.12 @@ -2152,7 +2152,7 @@
    4.13        measurable_restrict_space2[of f, of "restrict_space M A", of B, of N] assms(2) space_restrict_space)
    4.14  qed
    4.15  
    4.16 -text \<open>The next one is a variation around \verb+measurable_piecewise_restrict+.\<close>
    4.17 +text \<open>The next one is a variation around \<open>measurable_piecewise_restrict\<close>.\<close>
    4.18  
    4.19  lemma%important measurable_piecewise_restrict2:
    4.20    assumes [measurable]: "\<And>n. A n \<in> sets M"
     5.1 --- a/src/HOL/Analysis/Brouwer_Fixpoint.thy	Tue Jan 01 20:57:54 2019 +0100
     5.2 +++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy	Tue Jan 01 21:47:27 2019 +0100
     5.3 @@ -407,8 +407,8 @@
     5.4  retracts (ENR). We define AR and ANR by specializing the standard definitions for a set to embedding
     5.5  in spaces of higher dimension.
     5.6  
     5.7 -John Harrison writes: "This turns out to be sufficient (since any set in $\mathbb{R}^n$ can be
     5.8 -embedded as a closed subset of a convex subset of $\mathbb{R}^{n+1}$) to derive the usual
     5.9 +John Harrison writes: "This turns out to be sufficient (since any set in \<open>\<real>\<^sup>n\<close> can be
    5.10 +embedded as a closed subset of a convex subset of \<open>\<real>\<^sup>n\<^sup>+\<^sup>1\<close>) to derive the usual
    5.11  definitions, but we need to split them into two implications because of the lack of type
    5.12  quantifiers. Then ENR turns out to be equivalent to ANR plus local compactness."\<close>
    5.13  
     6.1 --- a/src/HOL/Analysis/Complete_Measure.thy	Tue Jan 01 20:57:54 2019 +0100
     6.2 +++ b/src/HOL/Analysis/Complete_Measure.thy	Tue Jan 01 21:47:27 2019 +0100
     6.3 @@ -1085,7 +1085,7 @@
     6.4  qed
     6.5  
     6.6  text \<open>The following theorem is a specialization of D.H. Fremlin, Measure Theory vol 4I (413G). We
     6.7 -  only show one direction and do not use a inner regular family $K$.\<close>
     6.8 +  only show one direction and do not use a inner regular family \<open>K\<close>.\<close>
     6.9  
    6.10  lemma (in cld_measure) borel_measurable_cld:
    6.11    fixes f :: "'a \<Rightarrow> real"
     7.1 --- a/src/HOL/Analysis/Complex_Transcendental.thy	Tue Jan 01 20:57:54 2019 +0100
     7.2 +++ b/src/HOL/Analysis/Complex_Transcendental.thy	Tue Jan 01 21:47:27 2019 +0100
     7.3 @@ -883,9 +883,9 @@
     7.4  qed
     7.5  
     7.6  text\<open>This function returns the angle of a complex number from its representation in polar coordinates.
     7.7 -Due to periodicity, its range is arbitrary. @{term Arg2pi} follows HOL Light in adopting the interval $[0,2\pi)$.
     7.8 +Due to periodicity, its range is arbitrary. @{term Arg2pi} follows HOL Light in adopting the interval \<open>[0,2\<pi>)\<close>.
     7.9  But we have the same periodicity issue with logarithms, and it is usual to adopt the same interval
    7.10 -for the complex logarithm and argument functions. Further on down, we shall define both functions for the interval $(-\pi,\pi]$.
    7.11 +for the complex logarithm and argument functions. Further on down, we shall define both functions for the interval \<open>(-\<pi>,\<pi>]\<close>.
    7.12  The present version is provided for compatibility.\<close>
    7.13  
    7.14  lemma Arg2pi_0 [simp]: "Arg2pi(0) = 0"
    7.15 @@ -1751,7 +1751,7 @@
    7.16  
    7.17  subsection\<open>The Argument of a Complex Number\<close>
    7.18  
    7.19 -text\<open>Finally: it's is defined for the same interval as the complex logarithm: $(-\pi,\pi]$.\<close>
    7.20 +text\<open>Finally: it's is defined for the same interval as the complex logarithm: \<open>(-\<pi>,\<pi>]\<close>.\<close>
    7.21  
    7.22  definition%important Arg :: "complex \<Rightarrow> real" where "Arg z \<equiv> (if z = 0 then 0 else Im (Ln z))"
    7.23  
     8.1 --- a/src/HOL/Analysis/Embed_Measure.thy	Tue Jan 01 20:57:54 2019 +0100
     8.2 +++ b/src/HOL/Analysis/Embed_Measure.thy	Tue Jan 01 21:47:27 2019 +0100
     8.3 @@ -14,7 +14,7 @@
     8.4  
     8.5  text \<open>
     8.6    Given a measure space on some carrier set \<open>\<Omega>\<close> and a function \<open>f\<close>, we can define a push-forward
     8.7 -  measure on the carrier set $f(\Omega)$ whose \<open>\<sigma>\<close>-algebra is the one generated by mapping \<open>f\<close> over
     8.8 +  measure on the carrier set \<open>f(\<Omega>)\<close> whose \<open>\<sigma>\<close>-algebra is the one generated by mapping \<open>f\<close> over
     8.9    the original sigma algebra.
    8.10  
    8.11    This is useful e.\,g.\ when \<open>f\<close> is injective, i.\,e.\ it is some kind of ``tagging'' function.
     9.1 --- a/src/HOL/Analysis/Extended_Real_Limits.thy	Tue Jan 01 20:57:54 2019 +0100
     9.2 +++ b/src/HOL/Analysis/Extended_Real_Limits.thy	Tue Jan 01 21:47:27 2019 +0100
     9.3 @@ -396,11 +396,11 @@
     9.4  
     9.5  subsubsection%important \<open>Continuity of addition\<close>
     9.6  
     9.7 -text \<open>The next few lemmas remove an unnecessary assumption in \verb+tendsto_add_ereal+, culminating
     9.8 -in \verb+tendsto_add_ereal_general+ which essentially says that the addition
     9.9 -is continuous on ereal times ereal, except at $(-\infty, \infty)$ and $(\infty, -\infty)$.
    9.10 +text \<open>The next few lemmas remove an unnecessary assumption in \<open>tendsto_add_ereal\<close>, culminating
    9.11 +in \<open>tendsto_add_ereal_general\<close> which essentially says that the addition
    9.12 +is continuous on ereal times ereal, except at \<open>(-\<infinity>, \<infinity>)\<close> and \<open>(\<infinity>, -\<infinity>)\<close>.
    9.13  It is much more convenient in many situations, see for instance the proof of
    9.14 -\verb+tendsto_sum_ereal+ below.\<close>
    9.15 +\<open>tendsto_sum_ereal\<close> below.\<close>
    9.16  
    9.17  lemma%important tendsto_add_ereal_PInf:
    9.18    fixes y :: ereal
    9.19 @@ -437,7 +437,7 @@
    9.20  qed
    9.21  
    9.22  text\<open>One would like to deduce the next lemma from the previous one, but the fact
    9.23 -that $-(x+y)$ is in general different from $(-x) + (-y)$ in ereal creates difficulties,
    9.24 +that \<open>- (x + y)\<close> is in general different from \<open>(- x) + (- y)\<close> in ereal creates difficulties,
    9.25  so it is more efficient to copy the previous proof.\<close>
    9.26  
    9.27  lemma%important tendsto_add_ereal_MInf:
    9.28 @@ -503,8 +503,8 @@
    9.29    ultimately show ?thesis by simp
    9.30  qed
    9.31  
    9.32 -text \<open>The next lemma says that the addition is continuous on ereal, except at
    9.33 -the pairs $(-\infty, \infty)$ and $(\infty, -\infty)$.\<close>
    9.34 +text \<open>The next lemma says that the addition is continuous on \<open>ereal\<close>, except at
    9.35 +the pairs \<open>(-\<infinity>, \<infinity>)\<close> and \<open>(\<infinity>, -\<infinity>)\<close>.\<close>
    9.36  
    9.37  lemma%important tendsto_add_ereal_general [tendsto_intros]:
    9.38    fixes x y :: ereal
    9.39 @@ -528,7 +528,7 @@
    9.40  subsubsection%important \<open>Continuity of multiplication\<close>
    9.41  
    9.42  text \<open>In the same way as for addition, we prove that the multiplication is continuous on
    9.43 -ereal times ereal, except at $(\infty, 0)$ and $(-\infty, 0)$ and $(0, \infty)$ and $(0, -\infty)$,
    9.44 +ereal times ereal, except at \<open>(\<infinity>, 0)\<close> and \<open>(-\<infinity>, 0)\<close> and \<open>(0, \<infinity>)\<close> and \<open>(0, -\<infinity>)\<close>,
    9.45  starting with specific situations.\<close>
    9.46  
    9.47  lemma%important tendsto_mult_real_ereal:
    9.48 @@ -922,7 +922,7 @@
    9.49    ultimately show ?thesis using MInf by auto
    9.50  qed (simp add: assms)
    9.51  
    9.52 -text \<open>the next one is copied from \verb+tendsto_sum+.\<close>
    9.53 +text \<open>the next one is copied from \<open>tendsto_sum\<close>.\<close>
    9.54  lemma tendsto_sum_ereal [tendsto_intros]:
    9.55    fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> ereal"
    9.56    assumes "\<And>i. i \<in> S \<Longrightarrow> (f i \<longlongrightarrow> a i) F"
    9.57 @@ -1476,8 +1476,8 @@
    9.58  qed
    9.59  
    9.60  text \<open>The following statement about limsups is reduced to a statement about limits using
    9.61 -subsequences thanks to \verb+limsup_subseq_lim+. The statement for limits follows for instance from
    9.62 -\verb+tendsto_add_ereal_general+.\<close>
    9.63 +subsequences thanks to \<open>limsup_subseq_lim\<close>. The statement for limits follows for instance from
    9.64 +\<open>tendsto_add_ereal_general\<close>.\<close>
    9.65  
    9.66  lemma%important ereal_limsup_add_mono:
    9.67    fixes u v::"nat \<Rightarrow> ereal"
    9.68 @@ -1521,7 +1521,7 @@
    9.69    then show ?thesis unfolding w_def by simp
    9.70  qed
    9.71  
    9.72 -text \<open>There is an asymmetry between liminfs and limsups in ereal, as $\infty + (-\infty) = \infty$.
    9.73 +text \<open>There is an asymmetry between liminfs and limsups in \<open>ereal\<close>, as \<open>\<infinity> + (-\<infinity>) = \<infinity>\<close>.
    9.74  This explains why there are more assumptions in the next lemma dealing with liminfs that in the
    9.75  previous one about limsups.\<close>
    9.76  
    10.1 --- a/src/HOL/Analysis/Function_Topology.thy	Tue Jan 01 20:57:54 2019 +0100
    10.2 +++ b/src/HOL/Analysis/Function_Topology.thy	Tue Jan 01 21:47:27 2019 +0100
    10.3 @@ -17,14 +17,14 @@
    10.4  to each factor is continuous.
    10.5  
    10.6  To form a product of objects in Isabelle/HOL, all these objects should be subsets of a common type
    10.7 -'a. The product is then @{term "Pi\<^sub>E I X"}, the set of elements from 'i to 'a such that the $i$-th
    10.8 -coordinate belongs to $X\;i$ for all $i \in I$.
    10.9 +'a. The product is then @{term "Pi\<^sub>E I X"}, the set of elements from \<open>'i\<close> to \<open>'a\<close> such that the \<open>i\<close>-th
   10.10 +coordinate belongs to \<open>X i\<close> for all \<open>i \<in> I\<close>.
   10.11  
   10.12  Hence, to form a product of topological spaces, all these spaces should be subsets of a common type.
   10.13  This means that type classes can not be used to define such a product if one wants to take the
   10.14  product of different topological spaces (as the type 'a can only be given one structure of
   10.15  topological space using type classes). On the other hand, one can define different topologies (as
   10.16 -introduced in \verb+thy+) on one type, and these topologies do not need to
   10.17 +introduced in \<open>thy\<close>) on one type, and these topologies do not need to
   10.18  share the same maximal open set. Hence, one can form a product of topologies in this sense, and
   10.19  this works well. The big caveat is that it does not interact well with the main body of
   10.20  topology in Isabelle/HOL defined in terms of type classes... For instance, continuity of maps
   10.21 @@ -41,25 +41,24 @@
   10.22  probably too naive here).
   10.23  
   10.24  Here is an example of a reformulation using topologies. Let
   10.25 -\begin{verbatim}
   10.26 -continuous_on_topo T1 T2 f = ((\<forall> U. openin T2 U \<longrightarrow> openin T1 (f-`U \<inter> topspace(T1)))
   10.27 -                                      \<and> (f`(topspace T1) \<subseteq> (topspace T2)))
   10.28 -\end{verbatim}
   10.29 -be the natural continuity definition of a map from the topology $T1$ to the topology $T2$. Then
   10.30 -the current \verb+continuous_on+ (with type classes) can be redefined as
   10.31 -\begin{verbatim}
   10.32 -continuous_on s f = continuous_on_topo (subtopology euclidean s) (topology euclidean) f
   10.33 -\end{verbatim}
   10.34 +@{text [display]
   10.35 +\<open>continuous_on_topo T1 T2 f =
   10.36 +    ((\<forall> U. openin T2 U \<longrightarrow> openin T1 (f-`U \<inter> topspace(T1)))
   10.37 +            \<and> (f`(topspace T1) \<subseteq> (topspace T2)))\<close>}
   10.38 +be the natural continuity definition of a map from the topology \<open>T1\<close> to the topology \<open>T2\<close>. Then
   10.39 +the current \<open>continuous_on\<close> (with type classes) can be redefined as
   10.40 +@{text [display] \<open>continuous_on s f =
   10.41 +    continuous_on_topo (subtopology euclidean s) (topology euclidean) f\<close>}
   10.42  
   10.43 -In fact, I need \verb+continuous_on_topo+ to express the continuity of the projection on subfactors
   10.44 -for the product topology, in Lemma~\verb+continuous_on_restrict_product_topology+, and I show
   10.45 -the above equivalence in Lemma~\verb+continuous_on_continuous_on_topo+.
   10.46 +In fact, I need \<open>continuous_on_topo\<close> to express the continuity of the projection on subfactors
   10.47 +for the product topology, in Lemma~\<open>continuous_on_restrict_product_topology\<close>, and I show
   10.48 +the above equivalence in Lemma~\<open>continuous_on_continuous_on_topo\<close>.
   10.49  
   10.50  I only develop the basics of the product topology in this theory. The most important missing piece
   10.51  is Tychonov theorem, stating that a product of compact spaces is always compact for the product
   10.52  topology, even when the product is not finite (or even countable).
   10.53  
   10.54 -I realized afterwards that this theory has a lot in common with \verb+Fin_Map.thy+.
   10.55 +I realized afterwards that this theory has a lot in common with \<^file>\<open>~~/src/HOL/Library/Finite_Map.thy\<close>.
   10.56  \<close>
   10.57  
   10.58  subsection%important \<open>Topology without type classes\<close>
   10.59 @@ -67,15 +66,15 @@
   10.60  subsubsection%important \<open>The topology generated by some (open) subsets\<close>
   10.61  
   10.62  text \<open>In the definition below of a generated topology, the \<open>Empty\<close> case is not necessary,
   10.63 -as it follows from \<open>UN\<close> taking for $K$ the empty set. However, it is convenient to have,
   10.64 +as it follows from \<open>UN\<close> taking for \<open>K\<close> the empty set. However, it is convenient to have,
   10.65  and is never a problem in proofs, so I prefer to write it down explicitly.
   10.66  
   10.67 -We do not require UNIV to be an open set, as this will not be the case in applications. (We are
   10.68 -thinking of a topology on a subset of UNIV, the remaining part of UNIV being irrelevant.)\<close>
   10.69 +We do not require \<open>UNIV\<close> to be an open set, as this will not be the case in applications. (We are
   10.70 +thinking of a topology on a subset of \<open>UNIV\<close>, the remaining part of \<open>UNIV\<close> being irrelevant.)\<close>
   10.71  
   10.72  inductive generate_topology_on for S where
   10.73 -Empty: "generate_topology_on S {}"
   10.74 -|Int: "generate_topology_on S a \<Longrightarrow> generate_topology_on S b \<Longrightarrow> generate_topology_on S (a \<inter> b)"
   10.75 +  Empty: "generate_topology_on S {}"
   10.76 +| Int: "generate_topology_on S a \<Longrightarrow> generate_topology_on S b \<Longrightarrow> generate_topology_on S (a \<inter> b)"
   10.77  | UN: "(\<And>k. k \<in> K \<Longrightarrow> generate_topology_on S k) \<Longrightarrow> generate_topology_on S (\<Union>K)"
   10.78  | Basis: "s \<in> S \<Longrightarrow> generate_topology_on S s"
   10.79  
   10.80 @@ -83,8 +82,8 @@
   10.81    "istopology (generate_topology_on S)"
   10.82  unfolding istopology_def by (auto intro: generate_topology_on.intros)
   10.83  
   10.84 -text \<open>The basic property of the topology generated by a set $S$ is that it is the
   10.85 -smallest topology containing all the elements of $S$:\<close>
   10.86 +text \<open>The basic property of the topology generated by a set \<open>S\<close> is that it is the
   10.87 +smallest topology containing all the elements of \<open>S\<close>:\<close>
   10.88  
   10.89  lemma%unimportant generate_topology_on_coarsest:
   10.90    assumes "istopology T"
   10.91 @@ -344,8 +343,8 @@
   10.92  we will need it to define the strong operator topology on the space of continuous linear operators,
   10.93  by pulling back the product topology on the space of all functions.\<close>
   10.94  
   10.95 -text \<open>\verb+pullback_topology A f T+ is the pullback of the topology $T$ by the map $f$ on
   10.96 -the set $A$.\<close>
   10.97 +text \<open>\<open>pullback_topology A f T\<close> is the pullback of the topology \<open>T\<close> by the map \<open>f\<close> on
   10.98 +the set \<open>A\<close>.\<close>
   10.99  
  10.100  definition%important pullback_topology::"('a set) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('b topology) \<Rightarrow> ('a topology)"
  10.101    where "pullback_topology A f T = topology (\<lambda>S. \<exists>U. openin T U \<and> S = f-`U \<inter> A)"
  10.102 @@ -434,7 +433,7 @@
  10.103  set along one single coordinate, and the whole space along other coordinates. In fact, this is only
  10.104  equivalent for nonempty products, but for the empty product the first formulation is better
  10.105  (the second one gives an empty product space, while an empty product should have exactly one
  10.106 -point, equal to \verb+undefined+ along all coordinates.
  10.107 +point, equal to \<open>undefined\<close> along all coordinates.
  10.108  
  10.109  So, we use the first formulation, which moreover seems to give rise to more straightforward proofs.
  10.110  \<close>
  10.111 @@ -970,7 +969,7 @@
  10.112                                                    "\<And>x i. open (A x i)"
  10.113                                                    "\<And>x S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> (\<exists>i. A x i \<subseteq> S)"
  10.114      by metis
  10.115 -  text \<open>$B i$ is a countable basis of neighborhoods of $x_i$.\<close>
  10.116 +  text \<open>\<open>B i\<close> is a countable basis of neighborhoods of \<open>x\<^sub>i\<close>.\<close>
  10.117    define B where "B = (\<lambda>i. (A (x i))`UNIV \<union> {UNIV})"
  10.118    have "countable (B i)" for i unfolding B_def by auto
  10.119  
  10.120 @@ -1119,13 +1118,13 @@
  10.121  
  10.122  subsection%important \<open>The strong operator topology on continuous linear operators\<close> (* FIX ME mv*)
  10.123  
  10.124 -text \<open>Let 'a and 'b be two normed real vector spaces. Then the space of linear continuous
  10.125 -operators from 'a to 'b has a canonical norm, and therefore a canonical corresponding topology
  10.126 -(the type classes instantiation are given in \verb+Bounded_Linear_Function.thy+).
  10.127 +text \<open>Let \<open>'a\<close> and \<open>'b\<close> be two normed real vector spaces. Then the space of linear continuous
  10.128 +operators from \<open>'a\<close> to \<open>'b\<close> has a canonical norm, and therefore a canonical corresponding topology
  10.129 +(the type classes instantiation are given in \<^file>\<open>Bounded_Linear_Function.thy\<close>).
  10.130  
  10.131 -However, there is another topology on this space, the strong operator topology, where $T_n$ tends to
  10.132 -$T$ iff, for all $x$ in 'a, then $T_n x$ tends to $T x$. This is precisely the product topology
  10.133 -where the target space is endowed with the norm topology. It is especially useful when 'b is the set
  10.134 +However, there is another topology on this space, the strong operator topology, where \<open>T\<^sub>n\<close> tends to
  10.135 +\<open>T\<close> iff, for all \<open>x\<close> in \<open>'a\<close>, then \<open>T\<^sub>n x\<close> tends to \<open>T x\<close>. This is precisely the product topology
  10.136 +where the target space is endowed with the norm topology. It is especially useful when \<open>'b\<close> is the set
  10.137  of real numbers, since then this topology is compact.
  10.138  
  10.139  We can not implement it using type classes as there is already a topology, but at least we
  10.140 @@ -1202,12 +1201,12 @@
  10.141  
  10.142  text \<open>In general, the product topology is not metrizable, unless the index set is countable.
  10.143  When the index set is countable, essentially any (convergent) combination of the metrics on the
  10.144 -factors will do. We use below the simplest one, based on $L^1$, but $L^2$ would also work,
  10.145 +factors will do. We use below the simplest one, based on \<open>L\<^sup>1\<close>, but \<open>L\<^sup>2\<close> would also work,
  10.146  for instance.
  10.147  
  10.148  What is not completely trivial is that the distance thus defined induces the same topology
  10.149  as the product topology. This is what we have to prove to show that we have an instance
  10.150 -of \verb+metric_space+.
  10.151 +of \<^class>\<open>metric_space\<close>.
  10.152  
  10.153  The proofs below would work verbatim for general countable products of metric spaces. However,
  10.154  since distances are only implemented in terms of type classes, we only develop the theory
  10.155 @@ -1476,10 +1475,10 @@
  10.156      by simp
  10.157  next
  10.158    text\<open>Finally, we show that the topology generated by the distance and the product
  10.159 -        topology coincide. This is essentially contained in Lemma \verb+fun_open_ball_aux+,
  10.160 +        topology coincide. This is essentially contained in Lemma \<open>fun_open_ball_aux\<close>,
  10.161          except that the condition to prove is expressed with filters. To deal with this,
  10.162 -        we copy some mumbo jumbo from Lemma \verb+eventually_uniformity_metric+ in
  10.163 -        \verb+Real_Vector_Spaces.thy+\<close>
  10.164 +        we copy some mumbo jumbo from Lemma \<open>eventually_uniformity_metric\<close> in
  10.165 +        \<^file>\<open>~~/src/HOL/Real_Vector_Spaces.thy\<close>\<close>
  10.166    fix U::"('a \<Rightarrow> 'b) set"
  10.167    have "eventually P uniformity \<longleftrightarrow> (\<exists>e>0. \<forall>x (y::('a \<Rightarrow> 'b)). dist x y < e \<longrightarrow> P (x, y))" for P
  10.168    unfolding uniformity_fun_def apply (subst eventually_INF_base)
  10.169 @@ -1581,7 +1580,7 @@
  10.170  text \<open>There are two natural sigma-algebras on a product space: the borel sigma algebra,
  10.171  generated by open sets in the product, and the product sigma algebra, countably generated by
  10.172  products of measurable sets along finitely many coordinates. The second one is defined and studied
  10.173 -in \verb+Finite_Product_Measure.thy+.
  10.174 +in \<^file>\<open>Finite_Product_Measure.thy\<close>.
  10.175  
  10.176  These sigma-algebra share a lot of natural properties (measurability of coordinates, for instance),
  10.177  but there is a fundamental difference: open sets are generated by arbitrary unions, not only
    11.1 --- a/src/HOL/Analysis/Further_Topology.thy	Tue Jan 01 20:57:54 2019 +0100
    11.2 +++ b/src/HOL/Analysis/Further_Topology.thy	Tue Jan 01 21:47:27 2019 +0100
    11.3 @@ -4188,7 +4188,7 @@
    11.4  
    11.5  subsection%important\<open>The "Borsukian" property of sets\<close>
    11.6  
    11.7 -text\<open>This doesn't have a standard name. Kuratowski uses ``contractible with respect to $[S^1]$''
    11.8 +text\<open>This doesn't have a standard name. Kuratowski uses ``contractible with respect to \<open>[S\<^sup>1]\<close>''
    11.9   while Whyburn uses ``property b''. It's closely related to unicoherence.\<close>
   11.10  
   11.11  definition%important Borsukian where
    12.1 --- a/src/HOL/Analysis/Gamma_Function.thy	Tue Jan 01 20:57:54 2019 +0100
    12.2 +++ b/src/HOL/Analysis/Gamma_Function.thy	Tue Jan 01 21:47:27 2019 +0100
    12.3 @@ -1799,10 +1799,10 @@
    12.4  
    12.5  text \<open>
    12.6    The following is a proof of the Bohr--Mollerup theorem, which states that
    12.7 -  any log-convex function $G$ on the positive reals that fulfils $G(1) = 1$ and
    12.8 -  satisfies the functional equation $G(x+1) = x G(x)$ must be equal to the
    12.9 +  any log-convex function \<open>G\<close> on the positive reals that fulfils \<open>G(1) = 1\<close> and
   12.10 +  satisfies the functional equation \<open>G(x + 1) = x G(x)\<close> must be equal to the
   12.11    Gamma function.
   12.12 -  In principle, if $G$ is a holomorphic complex function, one could then extend
   12.13 +  In principle, if \<open>G\<close> is a holomorphic complex function, one could then extend
   12.14    this from the positive reals to the entire complex plane (minus the non-positive
   12.15    integers, where the Gamma function is not defined).
   12.16  \<close>
    13.1 --- a/src/HOL/Analysis/Lipschitz.thy	Tue Jan 01 20:57:54 2019 +0100
    13.2 +++ b/src/HOL/Analysis/Lipschitz.thy	Tue Jan 01 21:47:27 2019 +0100
    13.3 @@ -423,9 +423,9 @@
    13.4  
    13.5  text \<open>We deduce that if a function is Lipschitz on finitely many closed sets on the real line, then
    13.6  it is Lipschitz on any interval contained in their union. The difficulty in the proof is to show
    13.7 -that any point $z$ in this interval (except the maximum) has a point arbitrarily close to it on its
    13.8 +that any point \<open>z\<close> in this interval (except the maximum) has a point arbitrarily close to it on its
    13.9  right which is contained in a common initial closed set. Otherwise, we show that there is a small
   13.10 -interval $(z, T)$ which does not intersect any of the initial closed sets, a contradiction.\<close>
   13.11 +interval \<open>(z, T)\<close> which does not intersect any of the initial closed sets, a contradiction.\<close>
   13.12  
   13.13  proposition lipschitz_on_closed_Union:
   13.14    assumes "\<And>i. i \<in> I \<Longrightarrow> lipschitz_on M (U i) f"
    14.1 --- a/src/HOL/Analysis/Measure_Space.thy	Tue Jan 01 20:57:54 2019 +0100
    14.2 +++ b/src/HOL/Analysis/Measure_Space.thy	Tue Jan 01 21:47:27 2019 +0100
    14.3 @@ -1093,7 +1093,7 @@
    14.4  qed
    14.5  
    14.6  text \<open>The next lemma is convenient to combine with a lemma whose conclusion is of the
    14.7 -form \<open>AE x in M. P x = Q x\<close>: for such a lemma, there is no \verb+[symmetric]+ variant,
    14.8 +form \<open>AE x in M. P x = Q x\<close>: for such a lemma, there is no \<open>[symmetric]\<close> variant,
    14.9  but using \<open>AE_symmetric[OF...]\<close> will replace it.\<close>
   14.10  
   14.11  (* depricated replace by laws about eventually *)
   14.12 @@ -3522,7 +3522,7 @@
   14.13    qed
   14.14  qed
   14.15  
   14.16 -subsubsection%unimportant \<open>Supremum of a set of $\sigma$-algebras\<close>
   14.17 +subsubsection%unimportant \<open>Supremum of a set of \<open>\<sigma>\<close>-algebras\<close>
   14.18  
   14.19  lemma space_Sup_eq_UN: "space (Sup M) = (\<Union>x\<in>M. space x)"
   14.20    unfolding Sup_measure_def
    15.1 --- a/src/HOL/Analysis/Path_Connected.thy	Tue Jan 01 20:57:54 2019 +0100
    15.2 +++ b/src/HOL/Analysis/Path_Connected.thy	Tue Jan 01 21:47:27 2019 +0100
    15.3 @@ -3401,9 +3401,9 @@
    15.4         (\<forall>x. h(1, x) = q x) \<and>
    15.5         (\<forall>t \<in> {0..1}. P(\<lambda>x. h(t, x))))"
    15.6  
    15.7 -text\<open>$p, q$ are functions $X \to Y$, and the property $P$ restricts all intermediate maps.
    15.8 -We often just want to require that $P$ fixes some subset, but to include the case of a loop homotopy,
    15.9 -it is convenient to have a general property $P$.\<close>
   15.10 +text\<open>\<open>p\<close>, \<open>q\<close> are functions \<open>X \<rightarrow> Y\<close>, and the property \<open>P\<close> restricts all intermediate maps.
   15.11 +We often just want to require that \<open>P\<close> fixes some subset, but to include the case of a loop homotopy,
   15.12 +it is convenient to have a general property \<open>P\<close>.\<close>
   15.13  
   15.14  text \<open>We often want to just localize the ending function equality or whatever.\<close>
   15.15  text%important \<open>%whitespace\<close>
    16.1 --- a/src/HOL/Analysis/Set_Integral.thy	Tue Jan 01 20:57:54 2019 +0100
    16.2 +++ b/src/HOL/Analysis/Set_Integral.thy	Tue Jan 01 21:47:27 2019 +0100
    16.3 @@ -817,7 +817,7 @@
    16.4    then show ?thesis using * by auto
    16.5  qed
    16.6  
    16.7 -text \<open>The next lemma shows that $L^1$ convergence of a sequence of functions follows from almost
    16.8 +text \<open>The next lemma shows that \<open>L\<^sup>1\<close> convergence of a sequence of functions follows from almost
    16.9  everywhere convergence and the weaker condition of the convergence of the integrated norms (or even
   16.10  just the nontrivial inequality about them). Useful in a lot of contexts! This statement (or its
   16.11  variations) are known as Scheffe lemma.
    17.1 --- a/src/HOL/Analysis/Sigma_Algebra.thy	Tue Jan 01 20:57:54 2019 +0100
    17.2 +++ b/src/HOL/Analysis/Sigma_Algebra.thy	Tue Jan 01 21:47:27 2019 +0100
    17.3 @@ -1431,7 +1431,7 @@
    17.4  
    17.5  subsubsection \<open>Induction rule for intersection-stable generators\<close>
    17.6  
    17.7 -text%important \<open>The reason to introduce Dynkin-systems is the following induction rules for $\sigma$-algebras
    17.8 +text%important \<open>The reason to introduce Dynkin-systems is the following induction rules for \<open>\<sigma>\<close>-algebras
    17.9  generated by a generator closed under intersection.\<close>
   17.10  
   17.11  proposition sigma_sets_induct_disjoint[consumes 3, case_names basic empty compl union]:
   17.12 @@ -2022,7 +2022,7 @@
   17.13    using emeasure_extend_measure[OF M _ _ ms(2,3), of "(i,j)"] eq ms(1) \<open>I i j\<close>
   17.14    by (auto simp: subset_eq)
   17.15  
   17.16 -subsection \<open>The smallest $\sigma$-algebra regarding a function\<close>
   17.17 +subsection \<open>The smallest \<open>\<sigma>\<close>-algebra regarding a function\<close>
   17.18  
   17.19  definition%important vimage_algebra :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b measure \<Rightarrow> 'a measure" where
   17.20    "vimage_algebra X f M = sigma X {f -` A \<inter> X | A. A \<in> sets M}"