-
Notifications
You must be signed in to change notification settings - Fork 193
Expand file tree
/
Copy pathPhyslibAlpha.lean
More file actions
237 lines (236 loc) · 17.6 KB
/
Copy pathPhyslibAlpha.lean
File metadata and controls
237 lines (236 loc) · 17.6 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
module
public import PhyslibAlpha.Basic
public import PhyslibAlpha.ClassicalFieldTheory.Local.FirstVariation
public import PhyslibAlpha.ClassicalFieldTheory.Local.Action
public import PhyslibAlpha.ClassicalFieldTheory.Local.EulerLagrange
public import PhyslibAlpha.ClassicalFieldTheory.Local.EulerLagrangeEquation
public import PhyslibAlpha.ClassicalFieldTheory.Local.FirstOrder
public import PhyslibAlpha.ClassicalFieldTheory.Local.FirstVariation.Basic
public import PhyslibAlpha.ClassicalFieldTheory.Local.FirstVariation.Criterion
public import PhyslibAlpha.ClassicalFieldTheory.Local.FirstVariation.Density
public import PhyslibAlpha.ClassicalFieldTheory.Local.FirstVariation.IntegrationByParts
public import PhyslibAlpha.ClassicalFieldTheory.Local.FirstVariation.Regularity
public import PhyslibAlpha.ClassicalFieldTheory.Local.FirstVariation.Support
public import PhyslibAlpha.ClassicalFieldTheory.Local.JetPoint
public import PhyslibAlpha.ClassicalFieldTheory.Local.JetPointFiber
public import PhyslibAlpha.ClassicalFieldTheory.Local.JetPointRegularity
public import PhyslibAlpha.ClassicalFieldTheory.Local.Lagrangian
public import PhyslibAlpha.ClassicalFieldTheory.Local.TotalDerivative
public import PhyslibAlpha.ClassicalFieldTheory.Local.TotalDivergence
public import PhyslibAlpha.ClassicalFieldTheory.Local.TotalDivergenceEquivalence
public import PhyslibAlpha.ClassicalFieldTheory.Local.Variation
public import PhyslibAlpha.SpaceAndTime.Space.Surfaces.HalfPlane
public import PhyslibAlpha.SpaceAndTime.Space.Surfaces.Line
public import PhyslibAlpha.SpaceAndTime.Space.Surfaces.Ring
public import PhyslibAlpha.SpaceAndTime.Space.Surfaces.SphericalCylinder
public import PhyslibAlpha.SpaceAndTime.Space.Surfaces.SolidCylinder
public import PhyslibAlpha.SpaceAndTime.Space.Surfaces.SolidSphere
public import PhyslibAlpha.SpaceAndTime.Space.Surfaces.SphericalShell
public import PhyslibAlpha.ClassicalMechanics.MomentMap.Basic
public import PhyslibAlpha.ClassicalMechanics.MomentMap.Cohomology
public import PhyslibAlpha.ClassicalMechanics.MomentMap.GalileanMass
public import PhyslibAlpha.ClassicalMechanics.NortonDome.Basic
public import PhyslibAlpha.ClassicalMechanics.NortonDome.Determinism
public import PhyslibAlpha.ClassicalMechanics.NortonDome.NewtonianSystem
public import PhyslibAlpha.ClassicalMechanics.NortonDome.PeanoExistence
public import PhyslibAlpha.ClassicalMechanics.NortonDome.PhysicalSpace
public import PhyslibAlpha.ClassicalMechanics.NortonDome.PosPartPow
public import PhyslibAlpha.ClassicalMechanics.NortonDome.Solution
public import PhyslibAlpha.ClassicalMechanics.NortonDome.Sqrt
public import PhyslibAlpha.QuantumMechanics.QuantumHarmonicOscillator
public import PhyslibAlpha.QuantumMechanics.HarmonicOscillator.Basic
public import PhyslibAlpha.QuantumMechanics.HarmonicOscillator.LadderOperators
public import PhyslibAlpha.QuantumMechanics.HarmonicOscillator.Vacuum
public import PhyslibAlpha.QuantumMechanics.StinespringDilation
public import PhyslibAlpha.Mathematics.PartialDerivativeTest
public import PhyslibAlpha.Mathematics.LadderSystem.Basic
public import PhyslibAlpha.Mathematics.LadderSystem.Vacuum
public import PhyslibAlpha.Mathematics.LadderSystem.Irreducibility
public import PhyslibAlpha.Mathematics.LadderSystem.OccupationBasis
public import PhyslibAlpha.Mathematics.LadderSystem.SymmetricPower
public import PhyslibAlpha.ClassicalMechanics.CoupledSpringPotential
public import PhyslibAlpha.Particles.BeyondTheStandardModel.TwoHDM.ChargeBalance
public import PhyslibAlpha.Particles.BeyondTheStandardModel.TwoHDM.EffectivePotential
public import PhyslibAlpha.Particles.BeyondTheStandardModel.TwoHDM.GaugeSlice
public import PhyslibAlpha.Particles.BeyondTheStandardModel.TwoHDM.GaugeTorus
public import PhyslibAlpha.Particles.BeyondTheStandardModel.TwoHDM.Invariants
public import PhyslibAlpha.Particles.BeyondTheStandardModel.TwoHDM.Module
public import PhyslibAlpha.Particles.BeyondTheStandardModel.TwoHDM.OrbitRepresentative
public import PhyslibAlpha.Particles.BeyondTheStandardModel.TwoHDM.SwapDoublet
public import PhyslibAlpha.AlgebraicFramework.OrderUnit.Basic
public import PhyslibAlpha.AlgebraicFramework.OrderUnit.Composite
public import PhyslibAlpha.AlgebraicFramework.OrderUnit.Norm
public import PhyslibAlpha.AlgebraicFramework.OrderUnit.MonotoneComplete
public import PhyslibAlpha.AlgebraicFramework.OrderUnit.Operation
public import PhyslibAlpha.AlgebraicFramework.OrderUnit.Symmetry
public import PhyslibAlpha.AlgebraicFramework.OrderUnit.Channel.Basic
public import PhyslibAlpha.AlgebraicFramework.OrderUnit.Channel.MeasureAndPrepare
public import PhyslibAlpha.AlgebraicFramework.OrderUnit.Channel.Normal
public import PhyslibAlpha.AlgebraicFramework.OrderUnit.Channel.Weight
public import PhyslibAlpha.AlgebraicFramework.OrderUnit.Effect.Basic
public import PhyslibAlpha.AlgebraicFramework.OrderUnit.Effect.EffectValuedMeasure
public import PhyslibAlpha.AlgebraicFramework.OrderUnit.Effect.BoundedIntegral
public import PhyslibAlpha.AlgebraicFramework.OrderUnit.Effect.Integral
public import PhyslibAlpha.AlgebraicFramework.OrderUnit.State.Basic
public import PhyslibAlpha.AlgebraicFramework.OrderUnit.State.Convex
public import PhyslibAlpha.AlgebraicFramework.OrderUnit.State.Discrimination
public import PhyslibAlpha.AlgebraicFramework.OrderUnit.State.Norm
public import PhyslibAlpha.AlgebraicFramework.OrderUnit.State.Pure
public import PhyslibAlpha.AlgebraicFramework.OrderUnit.State.Separation
public import PhyslibAlpha.AlgebraicFramework.OrderUnit.State.WeightEquivalence
public import PhyslibAlpha.AlgebraicFramework.OrderUnit.State.NormalEquivalence
public import PhyslibAlpha.AlgebraicFramework.OrderUnit.Weight.Basic
public import PhyslibAlpha.AlgebraicFramework.OrderUnit.Weight.Continuous
public import PhyslibAlpha.AlgebraicFramework.OrderUnit.Weight.Extension
public import PhyslibAlpha.AlgebraicFramework.StarAlgebra.Jordan
public import PhyslibAlpha.AlgebraicFramework.StarAlgebra.Lie
public import PhyslibAlpha.AlgebraicFramework.StarAlgebra.Observable
public import PhyslibAlpha.AlgebraicFramework.StarAlgebra.Restrict
public import PhyslibAlpha.AlgebraicFramework.StarAlgebra.SelfAdjoint
public import PhyslibAlpha.AlgebraicFramework.StarAlgebra.Statistics
public import PhyslibAlpha.AlgebraicFramework.StarAlgebra.Traciality
public import PhyslibAlpha.AlgebraicFramework.CStarAlgebra.Automorphism
public import PhyslibAlpha.AlgebraicFramework.CStarAlgebra.Channel
public import PhyslibAlpha.AlgebraicFramework.CStarAlgebra.ConjugationSymmetry
public import PhyslibAlpha.AlgebraicFramework.CStarAlgebra.GNS
public import PhyslibAlpha.AlgebraicFramework.CStarAlgebra.JordanDecomposition
public import PhyslibAlpha.AlgebraicFramework.CStarAlgebra.OrderUnit
public import PhyslibAlpha.AlgebraicFramework.CStarAlgebra.Projection
public import PhyslibAlpha.AlgebraicFramework.CStarAlgebra.SharpEffect
public import PhyslibAlpha.AlgebraicFramework.CStarAlgebra.SpectralMeasure
public import PhyslibAlpha.AlgebraicFramework.CStarAlgebra.Stinespring.Kernel
public import PhyslibAlpha.AlgebraicFramework.CStarAlgebra.Stinespring.Dilation
public import PhyslibAlpha.AlgebraicFramework.CStarAlgebra.Uncertainty
public import PhyslibAlpha.AlgebraicFramework.WStarAlgebra.Basic
public import PhyslibAlpha.AlgebraicFramework.WStarAlgebra.ConjSpace
public import PhyslibAlpha.AlgebraicFramework.HilbertSpace.Dynamics.Automorphism
public import PhyslibAlpha.AlgebraicFramework.HilbertSpace.Dynamics.Hamiltonian
public import PhyslibAlpha.AlgebraicFramework.HilbertSpace.Trace
public import PhyslibAlpha.AlgebraicFramework.HilbertSpace.TraceClass.Basic
public import PhyslibAlpha.AlgebraicFramework.HilbertSpace.TraceClass.HilbertSchmidt
public import PhyslibAlpha.AlgebraicFramework.HilbertSpace.TraceClass.Polar
public import PhyslibAlpha.AlgebraicFramework.HilbertSpace.TraceClass.GeneralIdeal
public import PhyslibAlpha.AlgebraicFramework.HilbertSpace.TraceClass.GeneralProduct
public import PhyslibAlpha.AlgebraicFramework.HilbertSpace.TraceClass.IdealNorm
public import PhyslibAlpha.AlgebraicFramework.HilbertSpace.TraceClass.Banach
public import PhyslibAlpha.AlgebraicFramework.HilbertSpace.TraceClass.TraceAlgebra
public import PhyslibAlpha.AlgebraicFramework.HilbertSpace.TraceClass.RankOne
public import PhyslibAlpha.AlgebraicFramework.HilbertSpace.TraceClass.Pairing
public import PhyslibAlpha.AlgebraicFramework.WStarAlgebra.BoundedSesquilinearForm
public import PhyslibAlpha.AlgebraicFramework.WStarAlgebra.TracePairingNorm
public import PhyslibAlpha.AlgebraicFramework.WStarAlgebra.TracePairingSurjectivity
public import PhyslibAlpha.AlgebraicFramework.WStarAlgebra.RankOnePairing
public import PhyslibAlpha.AlgebraicFramework.WStarAlgebra.Concrete
public import PhyslibAlpha.AlgebraicFramework.WStarAlgebra.Mathlib
public import PhyslibAlpha.AlgebraicFramework.HilbertSpace.Unbounded.Cayley.Basic
public import PhyslibAlpha.AlgebraicFramework.HilbertSpace.Unbounded.Cayley.Measure
public import PhyslibAlpha.AlgebraicFramework.HilbertSpace.Unbounded.Cayley.Certificate
public import PhyslibAlpha.AlgebraicFramework.HilbertSpace.Unbounded.Cayley.Inverse
public import PhyslibAlpha.AlgebraicFramework.HilbertSpace.Unbounded.Basic
public import PhyslibAlpha.AlgebraicFramework.HilbertSpace.Unbounded.ScalarMeasure
public import PhyslibAlpha.AlgebraicFramework.HilbertSpace.Unbounded.Conjugation
public import PhyslibAlpha.AlgebraicFramework.HilbertSpace.Unbounded.BoundedIntegral
public import PhyslibAlpha.AlgebraicFramework.HilbertSpace.Unbounded.BoundedIntegralAlgebra
public import PhyslibAlpha.AlgebraicFramework.HilbertSpace.Unbounded.StoneUnitaryGroup
public import PhyslibAlpha.AlgebraicFramework.HilbertSpace.Unbounded.WeakIntegral
public import PhyslibAlpha.AlgebraicFramework.HilbertSpace.Unbounded.RealAnalytic
public import PhyslibAlpha.AlgebraicFramework.HilbertSpace.Unbounded.AnalyticVector.Basic
public import PhyslibAlpha.AlgebraicFramework.HilbertSpace.Unbounded.AnalyticVector.Local
public import PhyslibAlpha.AlgebraicFramework.HilbertSpace.Unbounded.AnalyticVector.Nelson
public import PhyslibAlpha.AlgebraicFramework.HilbertSpace.Unbounded.Existence.CandidateGenerator
public import PhyslibAlpha.AlgebraicFramework.HilbertSpace.Unbounded.Existence.GeneratorInvariance
public import PhyslibAlpha.AlgebraicFramework.HilbertSpace.Unbounded.Existence.GenericGardingKernel
public import PhyslibAlpha.AlgebraicFramework.HilbertSpace.Unbounded.Existence.GardingVectors
public import PhyslibAlpha.AlgebraicFramework.HilbertSpace.Unbounded.Existence.GaussianKernelGrowth
public import PhyslibAlpha.AlgebraicFramework.HilbertSpace.Unbounded.Existence.IteratedKernelGrowth
public import PhyslibAlpha.AlgebraicFramework.HilbertSpace.Unbounded.Existence.GardingVectorWitness
public import PhyslibAlpha.AlgebraicFramework.HilbertSpace.Unbounded.Existence.StoneGenerator
public import PhyslibAlpha.AlgebraicFramework.HilbertSpace.Unbounded.Existence.StoneReconstruction
public import PhyslibAlpha.AlgebraicFramework.HilbertSpace.Unbounded.SelfAdjointSpectralTheorem
public import PhyslibAlpha.AlgebraicFramework.HilbertSpace.Unbounded.SpectralIntegral.Construction
public import PhyslibAlpha.AlgebraicFramework.HilbertSpace.Unbounded.SpectralIntegral.SpecTheorem
public import PhyslibAlpha.AlgebraicFramework.HilbertSpace.Unbounded.UnitaryInfra.SesquilinearForm
public import PhyslibAlpha.AlgebraicFramework.HilbertSpace.Unbounded.UnitaryInfra.SpectralMeasure
public import PhyslibAlpha.AlgebraicFramework.HilbertSpace.Unbounded.CayleySpectralData.Construction
public import PhyslibAlpha.AlgebraicFramework.HilbertSpace.Unbounded.CayleySpectralData.SpecTheorem
public import PhyslibAlpha.AlgebraicFramework.HilbertSpace.Unbounded.BoundedSelfAdjointData
public import PhyslibAlpha.AlgebraicFramework.HilbertSpace.Unbounded.SpectralPointMass
public import PhyslibAlpha.AlgebraicFramework.HilbertSpace.Unbounded.Stone
public import PhyslibAlpha.AlgebraicFramework.HilbertSpace.Unbounded.Flow.Stone
public import PhyslibAlpha.AlgebraicFramework.HilbertSpace.Unbounded.Flow.StoneAPI
public import PhyslibAlpha.AlgebraicFramework.HilbertSpace.Unbounded.Flow.StoneInvariance
public import PhyslibAlpha.AlgebraicFramework.HilbertSpace.Unbounded.EssentialSpectrum.Defs
public import PhyslibAlpha.AlgebraicFramework.HilbertSpace.Unbounded.EssentialSpectrum.WeakCompact
public import PhyslibAlpha.AlgebraicFramework.HilbertSpace.Unbounded.EssentialSpectrum.Closed
public import PhyslibAlpha.AlgebraicFramework.HilbertSpace.Unbounded.EssentialSpectrum.Smul
public import PhyslibAlpha.AlgebraicFramework.HilbertSpace.Unbounded.EssentialSpectrum.Weyl
public import PhyslibAlpha.AlgebraicFramework.HilbertSpace.Unbounded.EssentialSpectrum.Discrete
public import PhyslibAlpha.AlgebraicFramework.HilbertSpace.State.Density
public import PhyslibAlpha.AlgebraicFramework.HilbertSpace.State.DensityUncertainty
public import PhyslibAlpha.AlgebraicFramework.HilbertSpace.State.Vector
public import PhyslibAlpha.AlgebraicFramework.HilbertSpace.State.VectorUncertainty
public import PhyslibAlpha.AlgebraicFramework.Measurement.Basic
public import PhyslibAlpha.AlgebraicFramework.Measurement.ClassicalSystem
public import PhyslibAlpha.AlgebraicFramework.Measurement.Compatibility
public import PhyslibAlpha.AlgebraicFramework.Measurement.FiniteOutcome
public import PhyslibAlpha.AlgebraicFramework.Measurement.Instrument
public import PhyslibAlpha.AlgebraicFramework.Measurement.MeasurableOutcome
public import PhyslibAlpha.AlgebraicFramework.Measurement.BoundedScalarization
public import PhyslibAlpha.AlgebraicFramework.Measurement.Postprocessing
public import PhyslibAlpha.AlgebraicFramework.Measurement.ProbabilityLaw
public import PhyslibAlpha.AlgebraicFramework.Representation.PVM
public import PhyslibAlpha.AlgebraicFramework.Representation.Covariance.Basic
public import PhyslibAlpha.AlgebraicFramework.Representation.Covariance.Finite
public import PhyslibAlpha.AlgebraicFramework.Representation.Schur
public import PhyslibAlpha.AlgebraicFramework.JordanOrderUnit.Basic
public import PhyslibAlpha.AlgebraicFramework.JordanOrderUnit.Hom
public import PhyslibAlpha.AlgebraicFramework.JordanOrderUnit.FreeJordanTwo
public import PhyslibAlpha.AlgebraicFramework.JordanOrderUnit.Operator
public import PhyslibAlpha.AlgebraicFramework.JordanOrderUnit.Quadratic.Triple
public import PhyslibAlpha.AlgebraicFramework.JordanOrderUnit.Examples.SpinFactor
public import PhyslibAlpha.AlgebraicFramework.JordanOrderUnit.Observable
public import PhyslibAlpha.AlgebraicFramework.JordanOrderUnit.ProjectionResolution
public import PhyslibAlpha.AlgebraicFramework.JordanOrderUnit.Conditioning
public import PhyslibAlpha.AlgebraicFramework.JordanOrderUnit.Covariance
public import PhyslibAlpha.AlgebraicFramework.JordanOrderUnit.Compatibility
public import PhyslibAlpha.AlgebraicFramework.CStarAlgebra.JordanCompatibility
public import PhyslibAlpha.AlgebraicFramework.JordanOrderUnit.JB.Basic
public import PhyslibAlpha.AlgebraicFramework.CStarAlgebra.Jordan
public import PhyslibAlpha.AlgebraicFramework.JordanOrderUnit.Power.Associative
public import PhyslibAlpha.AlgebraicFramework.JordanOrderUnit.Power.Quadratic
public import PhyslibAlpha.AlgebraicFramework.JordanOrderUnit.Quadratic.Fundamental
public import PhyslibAlpha.AlgebraicFramework.JordanOrderUnit.Quadratic.Order
public import PhyslibAlpha.AlgebraicFramework.JordanOrderUnit.Quadratic.Operational
public import PhyslibAlpha.AlgebraicFramework.JordanOrderUnit.StructureAlgebra
public import PhyslibAlpha.AlgebraicFramework.JordanOrderUnit.FiniteRank
public import PhyslibAlpha.AlgebraicFramework.Algebra.Alternative
public import PhyslibAlpha.AlgebraicFramework.Algebra.NuclearInvolution
public import PhyslibAlpha.AlgebraicFramework.JordanOrderUnit.Quadratic.Projection
public import PhyslibAlpha.AlgebraicFramework.JordanOrderUnit.Power.GeneratedByOne
public import PhyslibAlpha.AlgebraicFramework.JordanOrderUnit.Power.Generated
public import PhyslibAlpha.AlgebraicFramework.JordanOrderUnit.FreeSpecialTwo
public import PhyslibAlpha.AlgebraicFramework.JordanOrderUnit.ShirshovWords
public import PhyslibAlpha.AlgebraicFramework.JordanOrderUnit.Power.Ring
public import PhyslibAlpha.AlgebraicFramework.Algebra.Derivation
public import PhyslibAlpha.AlgebraicFramework.Algebra.Statistics
public import PhyslibAlpha.AlgebraicFramework.Dynamics.OneParameterGroup
public import PhyslibAlpha.AlgebraicFramework.Dynamics.Generator
public import PhyslibAlpha.AlgebraicFramework.Dynamics.GeneratorIsDerivation
public import PhyslibAlpha.AlgebraicFramework.JordanOrderUnit.JB.Dynamics
public import PhyslibAlpha.AlgebraicFramework.JordanOrderUnit.JB.GeneratedByOne.Closed
public import PhyslibAlpha.AlgebraicFramework.JordanOrderUnit.JB.GeneratedByOne.Inherited
public import PhyslibAlpha.AlgebraicFramework.JordanOrderUnit.JB.GeneratedByOne.Spectrum
public import PhyslibAlpha.AlgebraicFramework.JordanOrderUnit.JB.GeneratedByOne.CFC
public import PhyslibAlpha.AlgebraicFramework.JordanOrderUnit.JB.GeneratedByOne.SquareRootUniqueness
public import PhyslibAlpha.AlgebraicFramework.JordanOrderUnit.JB.GeneratedByOne.Effect
public import PhyslibAlpha.AlgebraicFramework.JordanOrderUnit.Lueders
public import PhyslibAlpha.AlgebraicFramework.JordanOrderUnit.JB.GeneratedByOne.Uniform
public import PhyslibAlpha.AlgebraicFramework.JordanOrderUnit.JB.GeneratedByOne.PosInvertibility
public import PhyslibAlpha.AlgebraicFramework.JordanOrderUnit.JB.Order
public import PhyslibAlpha.AlgebraicFramework.JordanOrderUnit.JBW.Basic
public import PhyslibAlpha.AlgebraicFramework.JordanOrderUnit.JBW.ProjectionResolution
public import PhyslibAlpha.AlgebraicFramework.CStarAlgebra.JordanStatistics
public import PhyslibAlpha.AlgebraicFramework.CStarAlgebra.JordanPositivity
public import PhyslibAlpha.AlgebraicFramework.CStarAlgebra.JordanCFC
public import PhyslibAlpha.AlgebraicFramework.CStarAlgebra.JordanSpecial
public import PhyslibAlpha.Relativity.General.Schwarzschild.IncompressibleSphere