forked from leanprover-community/physlib
-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathPhyslibAlpha.lean
More file actions
151 lines (150 loc) · 11 KB
/
Copy pathPhyslibAlpha.lean
File metadata and controls
151 lines (150 loc) · 11 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
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.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.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.WeightBridge
public import PhyslibAlpha.AlgebraicFramework.OrderUnit.Weight.Basic
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.Uncertainty
public import PhyslibAlpha.AlgebraicFramework.WStarAlgebra.Basic
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.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.State.Density
public import PhyslibAlpha.AlgebraicFramework.HilbertSpace.State.Vector
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.Postprocessing
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.Relativity.General.Schwarzschild.IncompressibleSphere