Break out real-analysis from analysis (#1941)

This kept feeling a little weird.

Author: lowasser

src/analysis.lagda.md

@@ -3,32 +3,14 @@
 ```agda
 module analysis where
 
-open import analysis.absolute-convergence-series-real-numbers public
-open import analysis.addition-differentiable-real-maps-on-proper-closed-intervals-real-numbers public
 open import analysis.alternation-sequences-metric-abelian-groups public
-open import analysis.comparison-test-series-real-numbers public
 open import analysis.complete-metric-abelian-groups public
-open import analysis.composition-differentiable-real-functions-on-proper-closed-intervals-real-numbers public
-open import analysis.constructive-intermediate-value-theorem public
 open import analysis.convergent-series-complete-metric-abelian-groups public
 open import analysis.convergent-series-metric-abelian-groups public
-open import analysis.convergent-series-real-numbers public
-open import analysis.differentiability-constant-real-maps-on-proper-closed-intervals-real-numbers public
-open import analysis.differentiability-identity-map-on-proper-closed-intervals-real-numbers public
-open import analysis.differentiability-reciprocal-function-on-positive-proper-closed-intervals-real-numbers public
-open import analysis.differentiable-real-maps-on-proper-closed-intervals-real-numbers public
-open import analysis.intermediate-value-theorem public
 open import analysis.limits-of-sequences-metric-abelian-groups public
 open import analysis.metric-abelian-groups public
-open import analysis.metric-abelian-groups-normed-real-vector-spaces public
 open import analysis.metric-abelian-groups-of-uniformly-continuous-maps-into-metric-abelian-groups public
-open import analysis.monotone-convergence-theorem-increasing-sequences-real-numbers public
-open import analysis.multiplication-differentiable-real-functions-on-proper-closed-intervals-real-numbers public
-open import analysis.nonnegative-series-real-numbers public
-open import analysis.ratio-test-series-real-numbers public
-open import analysis.scalar-multiplication-differentiable-real-maps-on-proper-closed-intervals-real-numbers public
 open import analysis.sequences-metric-abelian-groups public
 open import analysis.series-complete-metric-abelian-groups public
 open import analysis.series-metric-abelian-groups public
-open import analysis.series-real-numbers public
 ```

src/functional-analysis.lagda.md

@@ -6,6 +6,7 @@ module functional-analysis where
 open import functional-analysis.absolute-convergence-series-real-banach-spaces public
 open import functional-analysis.additive-complete-metric-abelian-groups-real-banach-spaces public
 open import functional-analysis.convergent-series-real-banach-spaces public
+open import functional-analysis.metric-abelian-groups-normed-real-vector-spaces public
 open import functional-analysis.ratio-test-series-real-banach-spaces public
 open import functional-analysis.real-banach-spaces public
 open import functional-analysis.real-hilbert-spaces public

src/functional-analysis/absolute-convergence-series-real-banach-spaces.lagda.md

@@ -7,9 +7,6 @@ module functional-analysis.absolute-convergence-series-real-banach-spaces where
 <details><summary>Imports</summary>
 
 ```agda
-open import analysis.convergent-series-real-numbers
-open import analysis.series-real-numbers
-
 open import elementary-number-theory.addition-natural-numbers
 open import elementary-number-theory.inequality-natural-numbers
 open import elementary-number-theory.natural-numbers
@@ -34,6 +31,9 @@ open import metric-spaces.cauchy-sequences-metric-spaces
 
 open import order-theory.large-posets
 
+open import real-analysis.convergent-series-real-numbers
+open import real-analysis.series-real-numbers
+
 open import real-numbers.cauchy-sequences-real-numbers
 open import real-numbers.difference-real-numbers
 open import real-numbers.distance-real-numbers
@@ -50,7 +50,7 @@ A [series](functional-analysis.series-real-banach-spaces.md) `Σ aₙ` in a
 [real Banach space](functional-analysis.real-banach-spaces.md) is said to
 {{#concept "absolutely converge" WDID=Q332465 WD="absolute convergence" Agda=is-absolutely-convergent-prop-series-ℝ-Banach-Space Disambiguation="series in a real Banach space"}}
 if the series of norms `Σ ∥aₙ∥` is a
-[convergent series](analysis.convergent-series-real-numbers.md) of
+[convergent series](real-analysis.convergent-series-real-numbers.md) of
 [real numbers](real-numbers.dedekind-real-numbers.md).
 
 ## Definition
@@ -195,7 +195,7 @@ module _
 
 ## See also
 
-- [Absolute convergence of series of real numbers](analysis.absolute-convergence-series-real-numbers.md)
+- [Absolute convergence of series of real numbers](real-analysis.absolute-convergence-series-real-numbers.md)
 
 ## External links
 

src/functional-analysis/additive-complete-metric-abelian-groups-real-banach-spaces.lagda.md

@@ -9,13 +9,13 @@ module functional-analysis.additive-complete-metric-abelian-groups-real-banach-s
 ```agda
 open import analysis.complete-metric-abelian-groups
 open import analysis.metric-abelian-groups
-open import analysis.metric-abelian-groups-normed-real-vector-spaces
 
 open import foundation.dependent-pair-types
 open import foundation.identity-types
 open import foundation.subtypes
 open import foundation.universe-levels
 
+open import functional-analysis.metric-abelian-groups-normed-real-vector-spaces
 open import functional-analysis.real-banach-spaces
 
 open import real-numbers.metric-additive-group-of-real-numbers

src/functional-analysis/convergent-series-real-banach-spaces.lagda.md

@@ -9,8 +9,6 @@ module functional-analysis.convergent-series-real-banach-spaces where
 ```agda
 open import analysis.convergent-series-complete-metric-abelian-groups
 open import analysis.convergent-series-metric-abelian-groups
-open import analysis.convergent-series-real-numbers
-open import analysis.series-real-numbers
 
 open import foundation.dependent-pair-types
 open import foundation.function-types
@@ -31,6 +29,9 @@ open import lists.sequences
 open import metric-spaces.cauchy-sequences-metric-spaces
 open import metric-spaces.limits-of-sequences-metric-spaces
 
+open import real-analysis.convergent-series-real-numbers
+open import real-analysis.series-real-numbers
+
 open import real-numbers.dedekind-real-numbers
 open import real-numbers.distance-real-numbers
 open import real-numbers.metric-space-of-real-numbers

…roups-normed-real-vector-spaces.lagda.md …roups-normed-real-vector-spaces.lagda.mdsrc/analysis/metric-abelian-groups-normed-real-vector-spaces.lagda.md renamed to src/functional-analysis/metric-abelian-groups-normed-real-vector-spaces.lagda.md src/analysis/metric-abelian-groups-normed-real-vector-spaces.lagda.md renamed to src/functional-analysis/metric-abelian-groups-normed-real-vector-spaces.lagda.md

@@ -1,7 +1,7 @@
 # Metric abelian groups of normed real vector spaces
 
 ```agda
-module analysis.metric-abelian-groups-normed-real-vector-spaces where
+module functional-analysis.metric-abelian-groups-normed-real-vector-spaces where
 ```
 
 <details><summary>Imports</summary>

src/functional-analysis/ratio-test-series-real-banach-spaces.lagda.md

@@ -7,8 +7,6 @@ module functional-analysis.ratio-test-series-real-banach-spaces where
 <details><summary>Imports</summary>
 
 ```agda
-open import analysis.ratio-test-series-real-numbers
-
 open import elementary-number-theory.natural-numbers
 
 open import foundation.binary-transport
@@ -26,6 +24,8 @@ open import functional-analysis.series-real-banach-spaces
 
 open import logic.functoriality-existential-quantification
 
+open import real-analysis.ratio-test-series-real-numbers
+
 open import real-numbers.absolute-value-real-numbers
 open import real-numbers.inequality-real-numbers
 open import real-numbers.multiplication-real-numbers
@@ -39,7 +39,7 @@ open import real-numbers.strict-inequality-nonnegative-real-numbers
 
 To prove that a [series](functional-analysis.series-real-banach-spaces.md)
 `∑ aₙ` in a [real Banach space](functional-analysis.real-banach-spaces.md)
-[converges](analysis.series-real-numbers.md), it is sufficient to show that
+[converges](real-analysis.series-real-numbers.md), it is sufficient to show that
 [there exists](foundation.existential-quantification.md) a
 [nonnegative](real-numbers.nonnegative-real-numbers.md) real number `r`
 [less than](real-numbers.strict-inequality-real-numbers.md) 1 such that for all
@@ -113,4 +113,4 @@ module _
 
 ## See also
 
-- [The ratio test for series of real numbers](analysis.ratio-test-series-real-numbers.md)
+- [The ratio test for series of real numbers](real-analysis.ratio-test-series-real-numbers.md)

src/functional-analysis/series-real-banach-spaces.lagda.md

@@ -7,9 +7,7 @@ module functional-analysis.series-real-banach-spaces where
 <details><summary>Imports</summary>
 
 ```agda
-open import analysis.metric-abelian-groups-normed-real-vector-spaces
 open import analysis.series-metric-abelian-groups
-open import analysis.series-real-numbers
 
 open import elementary-number-theory.addition-natural-numbers
 open import elementary-number-theory.natural-numbers
@@ -18,9 +16,12 @@ open import foundation.function-types
 open import foundation.identity-types
 open import foundation.universe-levels
 
+open import functional-analysis.metric-abelian-groups-normed-real-vector-spaces
 open import functional-analysis.real-banach-spaces
 
 open import lists.sequences
+
+open import real-analysis.series-real-numbers
 ```
 
 </details>
@@ -31,8 +32,8 @@ A
 {{#concept "series" Disambiguation="in a real Banach space" Agda=series-ℝ-Banach-Space}}
 is a [series](analysis.series-metric-abelian-groups.md) in the
 [metric abelian group](analysis.metric-abelian-groups.md)
-[associated](analysis.metric-abelian-groups-normed-real-vector-spaces.md) with
-the underlying
+[associated](functional-analysis.metric-abelian-groups-normed-real-vector-spaces.md)
+with the underlying
 [normed real vector space](linear-algebra.normed-real-vector-spaces.md).
 
 ## Definition

src/literature/100-theorems.lagda.md

@@ -202,9 +202,9 @@ open import linear-algebra.cauchy-schwarz-inequality-real-inner-product-spaces u
 **Author:** [Louis Wasserman](https://github.com/lowasser)
 
 ```agda
-open import analysis.intermediate-value-theorem using
+open import real-analysis.intermediate-value-theorem using
   ( intermediate-value-theorem-ℝ)
-open import analysis.constructive-intermediate-value-theorem using
+open import real-analysis.constructive-intermediate-value-theorem using
   ( constructive-intermediate-value-theorem-ℝ)
 ```
 

src/literature/wikipedia-list-of-theorems.lagda.md

@@ -21,7 +21,7 @@ The theorems are ordered alphabetically, omitting leading definite articles
 **Author:** [Louis Wasserman](https://github.com/lowasser)
 
 ```agda
-open import analysis.absolute-convergence-series-real-numbers using
+open import real-analysis.absolute-convergence-series-real-numbers using
   ( is-convergent-is-absolutely-convergent-series-ℝ)
 open import functional-analysis.absolute-convergence-series-real-banach-spaces using
   ( is-convergent-is-absolutely-convergent-series-ℝ-Banach-Space)
@@ -152,9 +152,9 @@ open import group-theory.quotient-groups using
 **Author:** [Louis Wasserman](https://github.com/lowasser)
 
 ```agda
-open import analysis.intermediate-value-theorem using
+open import real-analysis.intermediate-value-theorem using
   ( intermediate-value-theorem-ℝ)
-open import analysis.constructive-intermediate-value-theorem using
+open import real-analysis.constructive-intermediate-value-theorem using
   ( constructive-intermediate-value-theorem-ℝ)
 ```
 
@@ -195,7 +195,7 @@ open import foundation.lawveres-fixed-point-theorem using
 **Author:** [Fredrik Bakke](https://www.ntnu.edu/employees/fredrik.bakke)
 
 ```agda
-open import analysis.monotone-convergence-theorem-increasing-sequences-real-numbers using
+open import real-analysis.monotone-convergence-theorem-increasing-sequences-real-numbers using
   ( is-limit-is-modulated-supremum-is-increasing-sequence-ℝ ;
     is-limit-is-supremum-is-increasing-sequence-ACℕ-ℝ)
 ```