Folland real analysis definition catalogue

Title: Real Analysis: Modern Techniques and Their Applications, second edition

Author: Gerald B. Folland

Zotero key: FAE4HS67

Citekey: Fol13

Source attachment: local-write-api-1783336781793-FAE4HS67_extracted.md

Chapter 0: Prologue

• Set — §0.1, The Language of Set Theory, p. 1
  • Set — Mathlib/Data/Set/Defs.lean
• Relation — §0.1, The Language of Set Theory, p. 1
  • Relation — Mathlib/Logic/Relation.lean
• Equivalence relation — §0.1, The Language of Set Theory, p. 1
  • Setoid — Mathlib/Data/Setoid/Basic.lean
• Mapping — §0.1, The Language of Set Theory, p. 1
  • Function — Mathlib/Logic/Function/Basic.lean
• Sequence — §0.1, The Language of Set Theory, p. 1
  • Function — Mathlib/Logic/Function/Basic.lean
• Cartesian product — §0.1, The Language of Set Theory, p. 1
  • Prod — Mathlib/Data/Prod/Basic.lean
• Partial order — §0.2, Orderings, p. 4
  • PartialOrder — Mathlib/Order/Defs/PartialOrder.lean
• Linear order — §0.2, Orderings, p. 4
  • LinearOrder — Mathlib/Order/Defs/LinearOrder.lean
• Well ordering — §0.2, Orderings, p. 4
  • IsWellOrder — Mathlib/Order/RelClasses.lean
• Cardinality — §0.3, Cardinality, p. 6
  • Cardinal — Mathlib/SetTheory/Cardinal/Defs.lean
• Countable set — §0.3, Cardinality, p. 6
  • Set.Countable — Mathlib/Data/Set/Countable.lean
• Ordinal number — §0.4, More about Well Ordered Sets, p. 9
  • Ordinal — Mathlib/SetTheory/Ordinal/Basic.lean
• Extended real number system — §0.5, The Extended Real Number System, p. 10
  • EReal — Mathlib/Data/EReal/Basic.lean
• Metric space — §0.6, Metric Spaces, p. 13
  • MetricSpace — Mathlib/Topology/MetricSpace/Defs.lean
• Open ball — §0.6, Metric Spaces, p. 13
  • Metric.ball — Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
• Open set — §0.6, Metric Spaces, p. 13
  • IsOpen — Mathlib/Topology/Defs/Basic.lean
• Closed set — §0.6, Metric Spaces, p. 13
  • IsClosed — Mathlib/Topology/Defs/Basic.lean
• Interior — §0.6, Metric Spaces, p. 13
  • interior — Mathlib/Topology/Defs/Basic.lean
• Closure — §0.6, Metric Spaces, p. 13
  • closure — Mathlib/Topology/Defs/Basic.lean
• Dense subset — §0.6, Metric Spaces, p. 13
  • Dense — Mathlib/Topology/Defs/Basic.lean
• Separable metric space — §0.6, Metric Spaces, p. 13
  • SeparableSpace — Mathlib/Topology/Bases.lean
• Cauchy sequence — §0.6, Metric Spaces, p. 13
  • CauchySeq — Mathlib/Topology/UniformSpace/Cauchy.lean
• Complete metric space — §0.6, Metric Spaces, p. 13
  • CompleteSpace — Mathlib/Topology/UniformSpace/Cauchy.lean
• Totally bounded set — §0.6, Metric Spaces, p. 13
  • TotallyBounded — Mathlib/Topology/UniformSpace/Cauchy.lean
• Compact set — §0.6, Metric Spaces, p. 13
  • IsCompact — Mathlib/Topology/Defs/Filter.lean

Chapter 1: Measures

• Algebra of sets — §1.2, Sigma-algebras, p. 21
  • Mathlib: MeasureTheory.IsSetAlgebra — Mathlib/MeasureTheory/SetAlgebra.lean
• Sigma-algebra — §1.2, Sigma-algebras, p. 21
  • MeasurableSpace — Mathlib/MeasureTheory/MeasurableSpace/Defs.lean
• Generated sigma-algebra — §1.2, Sigma-algebras, p. 21
  • MeasurableSpace.generateFrom — Mathlib/MeasureTheory/MeasurableSpace/Defs.lean
• Borel sigma-algebra — §1.2, Sigma-algebras, p. 21
  • borel — Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean
• Measurable space — §1.2, Sigma-algebras, p. 21
  • MeasurableSpace — Mathlib/MeasureTheory/MeasurableSpace/Defs.lean
• Measure — §1.3, Measures, p. 24
  • Measure — Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean
• Measure space — §1.3, Measures, p. 24
  • MeasureSpace — Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean
• Finite measure — §1.3, Measures, p. 24
  • IsFiniteMeasure — Mathlib/MeasureTheory/Measure/Typeclasses/Finite.lean
• Sigma-finite measure — §1.3, Measures, p. 24
  • SigmaFinite — Mathlib/MeasureTheory/Measure/Typeclasses/SFinite.lean
• Semifinite measure — §1.3, Measures, p. 24
• Complete measure — §1.3, Measures, p. 24
  • Measure.IsComplete — Mathlib/MeasureTheory/Measure/NullMeasurable.lean
• Outer measure — §1.4, Outer Measures, p. 28
  • OuterMeasure — Mathlib/MeasureTheory/OuterMeasure/Defs.lean
• Caratheodory measurable set — §1.4, Outer Measures, p. 28
  • OuterMeasure.caratheodory — Mathlib/MeasureTheory/OuterMeasure/Caratheodory.lean
• Lebesgue measure — §1.5, Borel Measures on the Real Line, p. 33
  • volume — Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean
• Lebesgue measurable set — §1.5, Borel Measures on the Real Line, p. 33
  • MeasurableSet — Mathlib/MeasureTheory/MeasurableSpace/Defs.lean
• Lebesgue-Stieltjes measure — §1.5, Borel Measures on the Real Line, p. 33
  • StieltjesFunction.measure — Mathlib/MeasureTheory/Measure/Stieltjes.lean

Chapter 2: Integration

• Measurable function — §2.1, Measurable Functions, p. 43
  • Measurable — Mathlib/MeasureTheory/MeasurableSpace/Defs.lean
• Borel measurable function — §2.1, Measurable Functions, p. 43
  • Measurable — Mathlib/MeasureTheory/MeasurableSpace/Defs.lean
• Simple function — §2.1, Measurable Functions, p. 43
  • MeasureTheory.SimpleFunc — Mathlib/MeasureTheory/Function/SimpleFunc.lean
• Integral of a nonnegative simple function — §2.2, Integration of Nonnegative Functions, p. 49
  • MeasureTheory.SimpleFunc.lintegral — Mathlib/MeasureTheory/Function/SimpleFunc.lean
• Integral of a nonnegative measurable function — §2.2, Integration of Nonnegative Functions, p. 49
  • MeasureTheory.lintegral — Mathlib/MeasureTheory/Integral/Lebesgue/Basic.lean
• Integrable complex function — §2.3, Integration of Complex Functions, p. 52
  • MeasureTheory.Integrable — Mathlib/MeasureTheory/Function/L1Space/Integrable.lean
• Integral of a complex function — §2.3, Integration of Complex Functions, p. 52
  • MeasureTheory.integral — Mathlib/MeasureTheory/Integral/Bochner/Basic.lean
• Almost everywhere — §2.3, Integration of Complex Functions, p. 52
  • ae — Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean
• Convergence almost everywhere — §2.4, Modes of Convergence, p. 60
  • Filter.Tendsto — Mathlib/Order/Filter/Defs.lean
• Convergence in measure — §2.4, Modes of Convergence, p. 60
  • MeasureTheory.TendstoInMeasure — Mathlib/MeasureTheory/Function/ConvergenceInMeasure.lean
• Convergence in L1 — §2.4, Modes of Convergence, p. 60
  • MeasureTheory.L1 — Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
• Product sigma-algebra — §2.5, Product Measures, p. 64
  • MeasurableSpace.prod — Mathlib/MeasureTheory/MeasurableSpace/Constructions.lean
• Product measure — §2.5, Product Measures, p. 64
  • Measure.prod — Mathlib/MeasureTheory/Measure/Prod.lean:171
• Section of a measurable set — §2.5, Product Measures, p. 64
• Lebesgue integral on Euclidean space — §2.6, The n-dimensional Lebesgue Integral, p. 70
  • MeasureTheory.integral — Mathlib/MeasureTheory/Integral/Bochner/Basic.lean
• Polar coordinates — §2.7, Integration in Polar Coordinates, p. 77
  • Complex.polarCoord — Mathlib/Analysis/SpecialFunctions/PolarCoord.lean

Chapter 3: Signed Measures and Differentiation

• Signed measure — §3.1, Signed Measures, p. 85
  • SignedMeasure — Mathlib/MeasureTheory/VectorMeasure/Basic.lean
• Positive set for a signed measure — §3.1, Signed Measures, p. 85
• Negative set for a signed measure — §3.1, Signed Measures, p. 85
• Mutually singular measures — §3.1, Signed Measures, p. 85
  • Measure.MutuallySingular — Mathlib/MeasureTheory/Measure/MutuallySingular.lean
• Total variation measure — §3.1, Signed Measures, p. 85
  • SignedMeasure.totalVariation — Mathlib/MeasureTheory/VectorMeasure/Decomposition/Jordan.lean
• Absolute continuity of measures — §3.2, The Lebesgue-Radon-Nikodym Theorem, p. 88
  • Measure.AbsolutelyContinuous — Mathlib/MeasureTheory/Measure/AbsolutelyContinuous.lean
• Radon-Nikodym derivative — §3.2, The Lebesgue-Radon-Nikodym Theorem, p. 88
  • Measure.rnDeriv — Mathlib/MeasureTheory/Measure/Decomposition/Lebesgue.lean
• Complex measure — §3.3, Complex Measures, p. 93
  • ComplexMeasure — Mathlib/MeasureTheory/Measure/Complex.lean
• Lebesgue point — §3.4, Differentiation on Euclidean Space, p. 95
• Function of bounded variation — §3.5, Functions of Bounded Variation, p. 100
  • BoundedVariationOn — Mathlib/Topology/EMetricSpace/BoundedVariation.lean
• Total variation function — §3.5, Functions of Bounded Variation, p. 100
  • variationOnFromTo — Mathlib/Topology/EMetricSpace/VariationOnFromTo.lean
• Absolutely continuous function — §3.5, Functions of Bounded Variation, p. 100
  • AbsolutelyContinuousOnInterval — Mathlib/MeasureTheory/Function/AbsolutelyContinuous.lean

Chapter 4: Point Set Topology

• Topological space — §4.1, Topological Spaces, p. 113
  • TopologicalSpace — Mathlib/Topology/Defs/Basic.lean
• Neighborhood — §4.1, Topological Spaces, p. 113
  • nhds — Mathlib/Topology/Defs/Filter.lean
• Base for a topology — §4.1, Topological Spaces, p. 113
  • IsTopologicalBasis — Mathlib/Topology/Bases.lean
• Subbase for a topology — §4.1, Topological Spaces, p. 113
  • TopologicalSpace.generateFrom — Mathlib/Topology/Order.lean
• Subspace topology — §4.1, Topological Spaces, p. 113
  • TopologicalSpace.induced — Mathlib/Topology/Defs/Induced.lean
• Product topology — §4.1, Topological Spaces, p. 113
  • instTopologicalSpaceProd — Mathlib/Topology/Constructions.lean
• Hausdorff space — §4.1, Topological Spaces, p. 113
  • T2Space — Mathlib/Topology/Separation/Hausdorff.lean
• Continuous map — §4.2, Continuous Maps, p. 119
  • Continuous — Mathlib/Topology/Defs/Basic.lean
• Homeomorphism — §4.2, Continuous Maps, p. 119
  • Homeomorph — Mathlib/Topology/Homeomorph/Defs.lean
• Quotient topology — §4.2, Continuous Maps, p. 119
  • TopologicalSpace.coinduced — Mathlib/Topology/Defs/Induced.lean
• Net — §4.3, Nets, p. 125
  • Mathlib: Filter — Mathlib/Order/Filter/Defs.lean
• Subnet — §4.3, Nets, p. 125
  • Mathlib: Filter.Tendsto — Mathlib/Order/Filter/Defs.lean
• Compact space — §4.4, Compact Spaces, p. 128
  • CompactSpace — Mathlib/Topology/Defs/Filter.lean
• Relatively compact set — §4.4, Compact Spaces, p. 128
  • Mathlib: IsCompact (closure s) — Mathlib/Topology/Separation/Basic.lean
• Locally compact space — §4.5, Locally Compact Hausdorff Spaces, p. 131
  • LocallyCompactSpace — Mathlib/Topology/Defs/Filter.lean
• One-point compactification — §4.5, Locally Compact Hausdorff Spaces, p. 131
  • OnePoint — Mathlib/Topology/Compactification/OnePoint/Basic.lean
• Compact-open topology — §4.5, Locally Compact Hausdorff Spaces, p. 131
  • ContinuousMap.compactOpen — Mathlib/Topology/CompactOpen.lean
• Uniform algebra — §4.7, The Stone-Weierstrass Theorem, p. 138
• Completely regular space — §4.8, Embeddings in Cubes, p. 143
  • CompletelyRegularSpace — Mathlib/Topology/Separation/CompletelyRegular.lean
• Normal space — §4.8, Embeddings in Cubes, p. 143
  • NormalSpace — Mathlib/Topology/Separation/Regular.lean

Chapter 5: Elements of Functional Analysis

• Normed vector space — §5.1, Normed Vector Spaces, p. 151
  • NormedSpace — Mathlib/Analysis/Normed/Module/Basic.lean
• Banach space — §5.1, Normed Vector Spaces, p. 151
  • CompleteSpace — Mathlib/Topology/UniformSpace/Cauchy.lean
• Bounded linear map — §5.1, Normed Vector Spaces, p. 151
  • ContinuousLinearMap — Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Basic.lean
• Operator norm — §5.1, Normed Vector Spaces, p. 151
  • ContinuousLinearMap.opNorm — Mathlib/Analysis/Normed/Operator/Basic.lean
• Linear functional — §5.2, Linear Functionals, p. 157
  • LinearMap — Mathlib/Algebra/Module/LinearMap/Defs.lean:85
• Dual space — §5.2, Linear Functionals, p. 157
  • NormedSpace.Dual — Mathlib/Analysis/Normed/Module/Dual.lean
• Weak topology — §5.2, Linear Functionals, p. 157
  • WeakBilin — Mathlib/Topology/Algebra/Module/Spaces/WeakBilin.lean:64
• Weak-star topology — §5.2, Linear Functionals, p. 157
  • WeakDual — Mathlib/Topology/Algebra/Module/WeakDual.lean
• Meager set — §5.3, The Baire Category Theorem and its Consequences, p. 161
  • IsMeagre — Mathlib/Topology/GDelta/Basic.lean
• Baire space — §5.3, The Baire Category Theorem and its Consequences, p. 161
  • BaireSpace — Mathlib/Topology/Defs/Basic.lean
• Topological vector space — §5.4, Topological Vector Spaces, p. 165
  • ContinuousSMul — Mathlib/Topology/Algebra/Module/Basic.lean
• Locally convex space — §5.4, Topological Vector Spaces, p. 165
  • LocallyConvexSpace — Mathlib/Topology/Algebra/Module/LocallyConvex.lean
• Seminorm — §5.4, Topological Vector Spaces, p. 165
  • Seminorm — Mathlib/Analysis/Seminorm.lean
• Inner product space — §5.5, Hilbert Spaces, p. 171
  • InnerProductSpace — Mathlib/Analysis/InnerProductSpace/Defs.lean
• Hilbert space — §5.5, Hilbert Spaces, p. 171
  • CompleteSpace — Mathlib/Topology/UniformSpace/Cauchy.lean
• Orthogonal complement — §5.5, Hilbert Spaces, p. 171
  • Submodule.orthogonal — Mathlib/Analysis/InnerProductSpace/Orthogonal.lean
• Orthonormal set — §5.5, Hilbert Spaces, p. 171
  • Orthonormal — Mathlib/Analysis/InnerProductSpace/Orthonormal.lean
• Complete orthonormal set — §5.5, Hilbert Spaces, p. 171
  • OrthonormalBasis — Mathlib/Analysis/InnerProductSpace/Orthonormal.lean

Chapter 6: Lp Spaces

• Lp space — §6.1, Basic Theory of Lp Spaces, p. 181
  • MeasureTheory.Lp — Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
• Essential supremum — §6.1, Basic Theory of Lp Spaces, p. 181
  • MeasureTheory.essSup — Mathlib/MeasureTheory/Function/EssSup.lean
• L-infinity space — §6.1, Basic Theory of Lp Spaces, p. 181
  • MeasureTheory.Lp — Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
• Conjugate exponents — §6.1, Basic Theory of Lp Spaces, p. 181
  • IsConjExponent — Mathlib/Analysis/MeanInequalities.lean
• Dual of an Lp space — §6.2, The Dual of Lp, p. 188
  • NormedSpace.Dual — Mathlib/Analysis/Normed/Module/Dual.lean
• Distribution function — §6.4, Distribution Functions and Weak Lp, p. 197
  • MeasureTheory.distribution — fpvandoorn/BonnAnalysis:BonnAnalysis/LorentzSpace.lean
• Weak Lp space — §6.4, Distribution Functions and Weak Lp, p. 197
  • MeasureTheory.Lorentz (q = ∞) — fpvandoorn/BonnAnalysis:BonnAnalysis/LorentzSpace.lean
• Analytic family of operators — §6.5, Interpolation of Lp Spaces, p. 200

Chapter 7: Radon Measures

• Positive linear functional on Cc(X) — §7.1, Positive Linear Functionals on Cc(X), p. 211
  • PositiveLinearMap — Mathlib/Algebra/Order/Module/PositiveLinearMap.lean
• Radon measure — §7.2, Regularity and Approximation Theorems, p. 216
  • Measure.IsRadon — Mathlib/MeasureTheory/Measure/Regular.lean
• Outer regular measure — §7.2, Regularity and Approximation Theorems, p. 216
  • Measure.OuterRegular — Mathlib/MeasureTheory/Measure/Regular.lean
• Inner regular measure — §7.2, Regularity and Approximation Theorems, p. 216
  • Measure.InnerRegular — Mathlib/MeasureTheory/Measure/Regular.lean
• C0(X) — §7.3, The Dual of C0(X), p. 221
  • CocompactMap — Mathlib/Topology/ContinuousMap/CocompactMap.lean
• Product of Radon measures — §7.4, Products of Radon Measures, p. 226
  • Measure.prod — Mathlib/MeasureTheory/Measure/Prod.lean:171

Chapter 8: Elements of Fourier Analysis

• Translation operator — §8.1, Preliminaries, p. 235
  • translate — Mathlib/Algebra/Group/Translate.lean
• Dilation operator — §8.1, Preliminaries, p. 235
• Convolution — §8.2, Convolutions, p. 239
  • MeasureTheory.convolution — Mathlib/Analysis/Convolution.lean
• Approximate identity — §8.2, Convolutions, p. 239
  • TauCeti.IsMollifier — TauCetiProject/TauCeti:TauCeti/RepresentationTheory/Compact/ApproximateIdentity.lean
• Fourier transform — §8.3, The Fourier Transform, p. 247
  • FourierTransform — Mathlib/Analysis/Fourier/Notation.lean
• Inverse Fourier transform — §8.3, The Fourier Transform, p. 247
  • FourierTransformInv — Mathlib/Analysis/Fourier/Notation.lean
• Fourier series — §8.4, Summation of Fourier Integrals and Series, p. 257
  • fourierCoeff — Mathlib/Analysis/Fourier/AddCircle.lean
• Summability kernel — §8.4, Summation of Fourier Integrals and Series, p. 257
• Fourier-Stieltjes transform — §8.6, Fourier Analysis of Measures, p. 270
  • MeasureTheory.charFun — Mathlib/MeasureTheory/Measure/CharacteristicFunction/Basic.lean
• Fundamental solution of a differential operator — §8.7, Applications to Partial Differential Equations, p. 273
  • DifferentialOperators.IsTemperedFundamentalSolution — facebookresearch/atlas-lean:Atlas/DifferentialAnalysis/code/DifferentialOperators.lean

Chapter 9: Elements of Distribution Theory

• Test function — §9.1, Distributions, p. 281
  • TestFunction — Mathlib/Analysis/Distribution/TestFunction.lean
• Distribution — §9.1, Distributions, p. 281
  • Distribution — Mathlib/Analysis/Distribution/Distribution.lean
• Distributional derivative — §9.1, Distributions, p. 281
  • Distribution.lineDerivCLM — Mathlib/Analysis/Distribution/Distribution.lean
• Support of a distribution — §9.1, Distributions, p. 281
  • dsupport — Mathlib/Analysis/Distribution/Support.lean
• Compactly supported distribution — §9.2, Compactly Supported, Tempered, and Periodic Distributions, p. 291
  • IsCompactlySupportedDistribution — facebookresearch/atlas-lean:Atlas/DifferentialAnalysis/code/WavefrontSet.lean
• Tempered distribution — §9.2, Compactly Supported, Tempered, and Periodic Distributions, p. 291
  • TemperedDistribution — Mathlib/Analysis/Distribution/TemperedDistribution.lean
• Periodic distribution — §9.2, Compactly Supported, Tempered, and Periodic Distributions, p. 291
• Fourier transform of a tempered distribution — §9.2, Compactly Supported, Tempered, and Periodic Distributions, p. 291
  • FourierTransform.fourierCLM — Mathlib/Analysis/Fourier/Notation.lean:181 (was TemperedDistribution.fourierTransformCLM, a deprecated alias)
• Sobolev space — §9.3, Sobolev Spaces, p. 301
  • TemperedDistribution.MemSobolev — Mathlib/Analysis/Distribution/Sobolev.lean
• Weak derivative — §9.3, Sobolev Spaces, p. 301
  • Distribution.lineDerivCLM — Mathlib/Analysis/Distribution/Distribution.lean

Chapter 10: Topics in Probability Theory

• Probability space — §10.1, Basic Concepts, p. 313
  • Measure.IsProbabilityMeasure — Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean
• Random variable — §10.1, Basic Concepts, p. 313
  • Measurable — Mathlib/MeasureTheory/MeasurableSpace/Defs.lean
• Distribution of a random variable — §10.1, Basic Concepts, p. 313
  • Measure.map — Mathlib/MeasureTheory/Measure/Map.lean
• Expectation — §10.1, Basic Concepts, p. 313
  • MeasureTheory.integral — Mathlib/MeasureTheory/Integral/Bochner/Basic.lean
• Independence — §10.1, Basic Concepts, p. 313
  • ProbabilityTheory.Indep — Mathlib/Probability/Independence/Basic.lean
• Identically distributed random variables — §10.1, Basic Concepts, p. 313
  • ProbabilityTheory.IdentDistrib — Mathlib/Probability/IdentDistrib.lean
• Convergence in probability — §10.1, Basic Concepts, p. 313
  • MeasureTheory.TendstoInMeasure — Mathlib/MeasureTheory/Function/ConvergenceInMeasure.lean
• Convergence in distribution — §10.1, Basic Concepts, p. 313
  • MeasureTheory.TendstoInDistribution — Mathlib/MeasureTheory/Function/ConvergenceInDistribution.lean
• Characteristic function — §10.3, The Central Limit Theorem, p. 325
  • Measure.charFun — Mathlib/MeasureTheory/Measure/CharacteristicFunction/Basic.lean
• Product probability space — §10.4, Construction of Sample Spaces, p. 328
  • Measure.prod — Mathlib/MeasureTheory/Measure/Prod.lean:171
• Wiener process — §10.5, The Wiener Process, p. 330
  • ProbabilityTheory.IsBrownianReal — Mathlib/Probability/BrownianMotion/Basic.lean

Chapter 11: More Measures and Integrals

• Topological group — §11.1, Topological Groups and Haar Measure, p. 339
  • IsTopologicalGroup — Mathlib/Topology/Algebra/Group/Defs.lean
• Left Haar measure — §11.1, Topological Groups and Haar Measure, p. 339
  • MeasureTheory.IsHaarMeasure — Mathlib/MeasureTheory/Group/Measure.lean
• Right Haar measure — §11.1, Topological Groups and Haar Measure, p. 339
  • MeasureTheory.IsMulRightInvariant — Mathlib/MeasureTheory/Group/Defs.lean
• Modular function — §11.1, Topological Groups and Haar Measure, p. 339
  • MeasureTheory.modularCharacter — Mathlib/MeasureTheory/Group/ModularCharacter.lean
• Hausdorff measure — §11.2, Hausdorff Measure, p. 348
  • MeasureTheory.hausdorffMeasure — Mathlib/MeasureTheory/Measure/Hausdorff.lean
• Hausdorff dimension — §11.2, Hausdorff Measure, p. 348
  • MeasureTheory.dimH — Mathlib/Topology/MetricSpace/HausdorffDimension.lean
• Similarity — §11.3, Self-similarity and Hausdorff Dimension, p. 355
  • Dilation — Mathlib/Topology/MetricSpace/Dilation.lean
• Self-similar set — §11.3, Self-similarity and Hausdorff Dimension, p. 355
• Differential form — §11.4, Integration on Manifolds, p. 361
  • DifferentialForm — (no Mathlib declaration)
• Integral of a differential form — §11.4, Integration on Manifolds, p. 361
  • curveIntegral, CurveIntegrable — Mathlib/MeasureTheory/Integral/CurveIntegral/Basic.lean ```

```