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
299 lines (298 loc) · 21.8 KB
/
Copy pathPhyslibAlpha.lean
File metadata and controls
299 lines (298 loc) · 21.8 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
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
module
public import PhyslibAlpha.Basic
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
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.ClassicalMechanics.CoupledSpringPotential
public import PhyslibAlpha.ClassicalMechanics.MomentMap.Basic
public import PhyslibAlpha.ClassicalMechanics.MomentMap.Cohomology
public import PhyslibAlpha.ClassicalMechanics.MomentMap.GalileanMass
public import PhyslibAlpha.ClassicalMechanics.MomentMap.GalileanMassCocycle
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.CondensedMatter.TightBindingChain.Current
public import PhyslibAlpha.CondensedMatter.TightBindingChain.CurrentEigenstates
public import PhyslibAlpha.CondensedMatter.TightBindingChain.MaxCurrentState
public import PhyslibAlpha.CondensedMatter.TightBindingChain.OpenBoundary
public import PhyslibAlpha.CondensedMatter.TightBindingChain.Uncertainty
public import PhyslibAlpha.Electromagnetism.BoxChargeConservation
public import PhyslibAlpha.Electromagnetism.Distributional.WireJunction
public import PhyslibAlpha.Mathematics.Analysis.Normed.HolderDual
public import PhyslibAlpha.Mathematics.Analysis.RealBounds
public import PhyslibAlpha.Mathematics.Convex.Choquet.BoundaryRepresentation
public import PhyslibAlpha.Mathematics.Convex.Choquet.ExtremePointDecomposition
public import PhyslibAlpha.Mathematics.Convex.Choquet.Mixture
public import PhyslibAlpha.Mathematics.Convex.Choquet.RepresentingMeasure
public import PhyslibAlpha.Mathematics.Convex.DominatedCone
public import PhyslibAlpha.Mathematics.Convex.LpBall
public import PhyslibAlpha.Mathematics.Geometry.Simplex
public import PhyslibAlpha.Mathematics.LadderSystem.Basic
public import PhyslibAlpha.Mathematics.LadderSystem.Irreducibility
public import PhyslibAlpha.Mathematics.LadderSystem.OccupationBasis
public import PhyslibAlpha.Mathematics.LadderSystem.SymmetricPower
public import PhyslibAlpha.Mathematics.LadderSystem.Vacuum
public import PhyslibAlpha.Mathematics.MeasureTheory.BoundedMeasurable
public import PhyslibAlpha.Mathematics.MeasureTheory.IntegrationFunctional
public import PhyslibAlpha.Mathematics.MeasureTheory.LiftingAndConditioning
public import PhyslibAlpha.Mathematics.MeasureTheory.PositiveFunctionalIntegral
public import PhyslibAlpha.Mathematics.MeasureTheory.RegularMeasure
public import PhyslibAlpha.Mathematics.Order.Freudenthal
public import PhyslibAlpha.Mathematics.Order.PositiveDual.Basic
public import PhyslibAlpha.Mathematics.Order.PositiveDual.Bidual
public import PhyslibAlpha.Mathematics.Order.PositiveDual.BidualLattice
public import PhyslibAlpha.Mathematics.Order.PositiveDual.Interpolation
public import PhyslibAlpha.Mathematics.Order.PositiveDual.Majorant
public import PhyslibAlpha.Mathematics.Order.PositiveDual.RieszKantorovich
public import PhyslibAlpha.Mathematics.Order.PositiveDual.UpperEnvelope
public import PhyslibAlpha.Mathematics.Order.StrongUnit
public import PhyslibAlpha.Mathematics.Order.VectorLattice
public import PhyslibAlpha.Mathematics.PartialDerivativeTest
public import PhyslibAlpha.Mathematics.Probability.Kernel.Factorization
public import PhyslibAlpha.Mathematics.Sublinear
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.ProbabilisticTheory.Algebra.Alternative
public import PhyslibAlpha.ProbabilisticTheory.Algebra.Derivation
public import PhyslibAlpha.ProbabilisticTheory.Algebra.NuclearInvolution
public import PhyslibAlpha.ProbabilisticTheory.Algebra.Statistics
public import PhyslibAlpha.ProbabilisticTheory.CStarAlgebra.Automorphism
public import PhyslibAlpha.ProbabilisticTheory.CStarAlgebra.Commutative
public import PhyslibAlpha.ProbabilisticTheory.CStarAlgebra.ConjugationSymmetry
public import PhyslibAlpha.ProbabilisticTheory.CStarAlgebra.GNS
public import PhyslibAlpha.ProbabilisticTheory.CStarAlgebra.JordanDecomposition
public import PhyslibAlpha.ProbabilisticTheory.CStarAlgebra.MatrixComposite
public import PhyslibAlpha.ProbabilisticTheory.CStarAlgebra.OrderUnit
public import PhyslibAlpha.ProbabilisticTheory.CStarAlgebra.Projection
public import PhyslibAlpha.ProbabilisticTheory.CStarAlgebra.QuantumChannel
public import PhyslibAlpha.ProbabilisticTheory.CStarAlgebra.SharpEffect
public import PhyslibAlpha.ProbabilisticTheory.CStarAlgebra.SpectralMeasure
public import PhyslibAlpha.ProbabilisticTheory.CStarAlgebra.Stinespring.Dilation
public import PhyslibAlpha.ProbabilisticTheory.CStarAlgebra.Stinespring.Kernel
public import PhyslibAlpha.ProbabilisticTheory.CStarAlgebra.Uncertainty
public import PhyslibAlpha.ProbabilisticTheory.Channel.Basic
public import PhyslibAlpha.ProbabilisticTheory.Channel.MeasureAndPrepare
public import PhyslibAlpha.ProbabilisticTheory.Channel.Normal
public import PhyslibAlpha.ProbabilisticTheory.Channel.Operation
public import PhyslibAlpha.ProbabilisticTheory.Channel.Symmetry
public import PhyslibAlpha.ProbabilisticTheory.Channel.Weight
public import PhyslibAlpha.ProbabilisticTheory.Classical.Basic
public import PhyslibAlpha.ProbabilisticTheory.Classical.BauerSimplex
public import PhyslibAlpha.ProbabilisticTheory.Classical.BoundedMeasurable
public import PhyslibAlpha.ProbabilisticTheory.Classical.Channel
public import PhyslibAlpha.ProbabilisticTheory.Classical.Compatibility
public import PhyslibAlpha.ProbabilisticTheory.Classical.EnsembleRefinement
public import PhyslibAlpha.ProbabilisticTheory.Classical.FiniteDimensional
public import PhyslibAlpha.ProbabilisticTheory.Classical.FiniteSystem
public import PhyslibAlpha.ProbabilisticTheory.Classical.LatticeObservables
public import PhyslibAlpha.ProbabilisticTheory.Classical.NamiokaPhelps
public import PhyslibAlpha.ProbabilisticTheory.Classical.NormalStates
public import PhyslibAlpha.ProbabilisticTheory.Classical.Nuclear
public import PhyslibAlpha.ProbabilisticTheory.Classical.PureState
public import PhyslibAlpha.ProbabilisticTheory.Classical.SeparableObservables
public import PhyslibAlpha.ProbabilisticTheory.Classical.SimplexStateSpace
public import PhyslibAlpha.ProbabilisticTheory.Classical.UniqueDecomposition
public import PhyslibAlpha.ProbabilisticTheory.Composite.CompletePositivity
public import PhyslibAlpha.ProbabilisticTheory.Composite.TensorCone
public import PhyslibAlpha.ProbabilisticTheory.Dynamics.Generator
public import PhyslibAlpha.ProbabilisticTheory.Dynamics.GeneratorIsDerivation
public import PhyslibAlpha.ProbabilisticTheory.Dynamics.OneParameterGroup
public import PhyslibAlpha.ProbabilisticTheory.Effect.Basic
public import PhyslibAlpha.ProbabilisticTheory.Examples.GBit
public import PhyslibAlpha.ProbabilisticTheory.Examples.NormCone
public import PhyslibAlpha.ProbabilisticTheory.Examples.Qubit
public import PhyslibAlpha.ProbabilisticTheory.Examples.Square
public import PhyslibAlpha.ProbabilisticTheory.HilbertSpace.Dynamics.Automorphism
public import PhyslibAlpha.ProbabilisticTheory.HilbertSpace.Dynamics.Hamiltonian
public import PhyslibAlpha.ProbabilisticTheory.HilbertSpace.State.Density
public import PhyslibAlpha.ProbabilisticTheory.HilbertSpace.State.DensityUncertainty
public import PhyslibAlpha.ProbabilisticTheory.HilbertSpace.State.Vector
public import PhyslibAlpha.ProbabilisticTheory.HilbertSpace.State.VectorUncertainty
public import PhyslibAlpha.ProbabilisticTheory.HilbertSpace.Trace
public import PhyslibAlpha.ProbabilisticTheory.HilbertSpace.TraceClass.Banach
public import PhyslibAlpha.ProbabilisticTheory.HilbertSpace.TraceClass.Basic
public import PhyslibAlpha.ProbabilisticTheory.HilbertSpace.TraceClass.GeneralIdeal
public import PhyslibAlpha.ProbabilisticTheory.HilbertSpace.TraceClass.GeneralProduct
public import PhyslibAlpha.ProbabilisticTheory.HilbertSpace.TraceClass.HilbertSchmidt
public import PhyslibAlpha.ProbabilisticTheory.HilbertSpace.TraceClass.IdealNorm
public import PhyslibAlpha.ProbabilisticTheory.HilbertSpace.TraceClass.Pairing
public import PhyslibAlpha.ProbabilisticTheory.HilbertSpace.TraceClass.Polar
public import PhyslibAlpha.ProbabilisticTheory.HilbertSpace.TraceClass.RankOne
public import PhyslibAlpha.ProbabilisticTheory.HilbertSpace.TraceClass.TraceAlgebra
public import PhyslibAlpha.ProbabilisticTheory.HilbertSpace.Unbounded.AnalyticVector.Basic
public import PhyslibAlpha.ProbabilisticTheory.HilbertSpace.Unbounded.AnalyticVector.Local
public import PhyslibAlpha.ProbabilisticTheory.HilbertSpace.Unbounded.AnalyticVector.Nelson
public import PhyslibAlpha.ProbabilisticTheory.HilbertSpace.Unbounded.Basic
public import PhyslibAlpha.ProbabilisticTheory.HilbertSpace.Unbounded.BoundedIntegral
public import PhyslibAlpha.ProbabilisticTheory.HilbertSpace.Unbounded.BoundedIntegralAlgebra
public import PhyslibAlpha.ProbabilisticTheory.HilbertSpace.Unbounded.BoundedSelfAdjointData
public import PhyslibAlpha.ProbabilisticTheory.HilbertSpace.Unbounded.Cayley.Basic
public import PhyslibAlpha.ProbabilisticTheory.HilbertSpace.Unbounded.Cayley.Certificate
public import PhyslibAlpha.ProbabilisticTheory.HilbertSpace.Unbounded.Cayley.Inverse
public import PhyslibAlpha.ProbabilisticTheory.HilbertSpace.Unbounded.Cayley.Measure
public import PhyslibAlpha.ProbabilisticTheory.HilbertSpace.Unbounded.CayleySpectralData.Basic
public import PhyslibAlpha.ProbabilisticTheory.HilbertSpace.Unbounded.CayleySpectralData.SpecTheorem
public import PhyslibAlpha.ProbabilisticTheory.HilbertSpace.Unbounded.Conjugation
public import PhyslibAlpha.ProbabilisticTheory.HilbertSpace.Unbounded.EssentialSpectrum.Closed
public import PhyslibAlpha.ProbabilisticTheory.HilbertSpace.Unbounded.EssentialSpectrum.Defs
public import PhyslibAlpha.ProbabilisticTheory.HilbertSpace.Unbounded.EssentialSpectrum.Smul
public import PhyslibAlpha.ProbabilisticTheory.HilbertSpace.Unbounded.EssentialSpectrum.WeakCompact
public import PhyslibAlpha.ProbabilisticTheory.HilbertSpace.Unbounded.EssentialSpectrum.Weyl
public import PhyslibAlpha.ProbabilisticTheory.HilbertSpace.Unbounded.Existence.CandidateGenerator
public import PhyslibAlpha.ProbabilisticTheory.HilbertSpace.Unbounded.Existence.GardingVectorWitness
public import PhyslibAlpha.ProbabilisticTheory.HilbertSpace.Unbounded.Existence.GardingVectors
public import PhyslibAlpha.ProbabilisticTheory.HilbertSpace.Unbounded.Existence.GaussianKernelGrowth
public import PhyslibAlpha.ProbabilisticTheory.HilbertSpace.Unbounded.Existence.GeneratorInvariance
public import PhyslibAlpha.ProbabilisticTheory.HilbertSpace.Unbounded.Existence.GenericGardingKernel
public import PhyslibAlpha.ProbabilisticTheory.HilbertSpace.Unbounded.Existence.IteratedKernelGrowth
public import PhyslibAlpha.ProbabilisticTheory.HilbertSpace.Unbounded.Existence.StoneGenerator
public import PhyslibAlpha.ProbabilisticTheory.HilbertSpace.Unbounded.Existence.StoneReconstruction
public import PhyslibAlpha.ProbabilisticTheory.HilbertSpace.Unbounded.Flow.Stone
public import PhyslibAlpha.ProbabilisticTheory.HilbertSpace.Unbounded.Flow.StoneAPI
public import PhyslibAlpha.ProbabilisticTheory.HilbertSpace.Unbounded.Flow.StoneInvariance
public import PhyslibAlpha.ProbabilisticTheory.HilbertSpace.Unbounded.RealAnalytic
public import PhyslibAlpha.ProbabilisticTheory.HilbertSpace.Unbounded.ScalarMeasure
public import PhyslibAlpha.ProbabilisticTheory.HilbertSpace.Unbounded.SelfAdjointSpectralTheorem
public import PhyslibAlpha.ProbabilisticTheory.HilbertSpace.Unbounded.SpectralIntegral.Construction
public import PhyslibAlpha.ProbabilisticTheory.HilbertSpace.Unbounded.SpectralIntegral.SpecTheorem
public import PhyslibAlpha.ProbabilisticTheory.HilbertSpace.Unbounded.SpectralPointMass
public import PhyslibAlpha.ProbabilisticTheory.HilbertSpace.Unbounded.Stone
public import PhyslibAlpha.ProbabilisticTheory.HilbertSpace.Unbounded.StoneUnitaryGroup
public import PhyslibAlpha.ProbabilisticTheory.HilbertSpace.Unbounded.UnitaryInfra.SesquilinearForm
public import PhyslibAlpha.ProbabilisticTheory.HilbertSpace.Unbounded.UnitaryInfra.SpectralMeasure
public import PhyslibAlpha.ProbabilisticTheory.HilbertSpace.Unbounded.WeakIntegral
public import PhyslibAlpha.ProbabilisticTheory.JordanOrderUnit.Basic
public import PhyslibAlpha.ProbabilisticTheory.JordanOrderUnit.CStarAlgebra.Basic
public import PhyslibAlpha.ProbabilisticTheory.JordanOrderUnit.CStarAlgebra.CFC
public import PhyslibAlpha.ProbabilisticTheory.JordanOrderUnit.CStarAlgebra.Compatibility
public import PhyslibAlpha.ProbabilisticTheory.JordanOrderUnit.CStarAlgebra.Positivity
public import PhyslibAlpha.ProbabilisticTheory.JordanOrderUnit.CStarAlgebra.Special
public import PhyslibAlpha.ProbabilisticTheory.JordanOrderUnit.CStarAlgebra.Statistics
public import PhyslibAlpha.ProbabilisticTheory.JordanOrderUnit.Compatibility
public import PhyslibAlpha.ProbabilisticTheory.JordanOrderUnit.Conditioning
public import PhyslibAlpha.ProbabilisticTheory.JordanOrderUnit.Covariance
public import PhyslibAlpha.ProbabilisticTheory.JordanOrderUnit.Examples.SpinFactor
public import PhyslibAlpha.ProbabilisticTheory.JordanOrderUnit.FiniteRank
public import PhyslibAlpha.ProbabilisticTheory.JordanOrderUnit.Hom
public import PhyslibAlpha.ProbabilisticTheory.JordanOrderUnit.JB.Basic
public import PhyslibAlpha.ProbabilisticTheory.JordanOrderUnit.JB.Dynamics
public import PhyslibAlpha.ProbabilisticTheory.JordanOrderUnit.JB.GeneratedByOne.CFC
public import PhyslibAlpha.ProbabilisticTheory.JordanOrderUnit.JB.GeneratedByOne.Closed
public import PhyslibAlpha.ProbabilisticTheory.JordanOrderUnit.JB.GeneratedByOne.Effect
public import PhyslibAlpha.ProbabilisticTheory.JordanOrderUnit.JB.GeneratedByOne.Inherited
public import PhyslibAlpha.ProbabilisticTheory.JordanOrderUnit.JB.GeneratedByOne.PosInvertibility
public import PhyslibAlpha.ProbabilisticTheory.JordanOrderUnit.JB.GeneratedByOne.Spectrum
public import PhyslibAlpha.ProbabilisticTheory.JordanOrderUnit.JB.GeneratedByOne.SqrtUniqueness
public import PhyslibAlpha.ProbabilisticTheory.JordanOrderUnit.JB.GeneratedByOne.Uniform
public import PhyslibAlpha.ProbabilisticTheory.JordanOrderUnit.JB.Order
public import PhyslibAlpha.ProbabilisticTheory.JordanOrderUnit.JBW.Basic
public import PhyslibAlpha.ProbabilisticTheory.JordanOrderUnit.JBW.ProjectionResolution
public import PhyslibAlpha.ProbabilisticTheory.JordanOrderUnit.Lueders
public import PhyslibAlpha.ProbabilisticTheory.JordanOrderUnit.Observable
public import PhyslibAlpha.ProbabilisticTheory.JordanOrderUnit.Operator
public import PhyslibAlpha.ProbabilisticTheory.JordanOrderUnit.Power.Associative
public import PhyslibAlpha.ProbabilisticTheory.JordanOrderUnit.Power.Generated
public import PhyslibAlpha.ProbabilisticTheory.JordanOrderUnit.Power.GeneratedByOne
public import PhyslibAlpha.ProbabilisticTheory.JordanOrderUnit.Power.Quadratic
public import PhyslibAlpha.ProbabilisticTheory.JordanOrderUnit.Power.Ring
public import PhyslibAlpha.ProbabilisticTheory.JordanOrderUnit.ProjectionResolution
public import PhyslibAlpha.ProbabilisticTheory.JordanOrderUnit.Quadratic.Fundamental
public import PhyslibAlpha.ProbabilisticTheory.JordanOrderUnit.Quadratic.Operational
public import PhyslibAlpha.ProbabilisticTheory.JordanOrderUnit.Quadratic.Order
public import PhyslibAlpha.ProbabilisticTheory.JordanOrderUnit.Quadratic.Projection
public import PhyslibAlpha.ProbabilisticTheory.JordanOrderUnit.Quadratic.Triple
public import PhyslibAlpha.ProbabilisticTheory.JordanOrderUnit.StructureAlgebra
public import PhyslibAlpha.ProbabilisticTheory.Measurement.Basic
public import PhyslibAlpha.ProbabilisticTheory.Measurement.Binary
public import PhyslibAlpha.ProbabilisticTheory.Measurement.BornRule
public import PhyslibAlpha.ProbabilisticTheory.Measurement.BoundedIntegral
public import PhyslibAlpha.ProbabilisticTheory.Measurement.BoundedScalarization
public import PhyslibAlpha.ProbabilisticTheory.Measurement.Compatibility
public import PhyslibAlpha.ProbabilisticTheory.Measurement.EffectValuedMeasure
public import PhyslibAlpha.ProbabilisticTheory.Measurement.Finite
public import PhyslibAlpha.ProbabilisticTheory.Measurement.Instrument
public import PhyslibAlpha.ProbabilisticTheory.Measurement.Integral
public import PhyslibAlpha.ProbabilisticTheory.Measurement.Postprocessing
public import PhyslibAlpha.ProbabilisticTheory.Measurement.Pushforward
public import PhyslibAlpha.ProbabilisticTheory.OrderUnit.Bidual
public import PhyslibAlpha.ProbabilisticTheory.OrderUnit.Interpolation
public import PhyslibAlpha.ProbabilisticTheory.OrderUnit.Lattice
public import PhyslibAlpha.ProbabilisticTheory.OrderUnit.MonotoneComplete
public import PhyslibAlpha.ProbabilisticTheory.OrderUnit.Normed
public import PhyslibAlpha.ProbabilisticTheory.OrderUnit.PositiveDual
public import PhyslibAlpha.ProbabilisticTheory.Representation.Covariance.Basic
public import PhyslibAlpha.ProbabilisticTheory.Representation.Covariance.Outcome
public import PhyslibAlpha.ProbabilisticTheory.Representation.PVM
public import PhyslibAlpha.ProbabilisticTheory.Representation.Schur
public import PhyslibAlpha.ProbabilisticTheory.StarAlgebra.Jordan
public import PhyslibAlpha.ProbabilisticTheory.StarAlgebra.Lie
public import PhyslibAlpha.ProbabilisticTheory.StarAlgebra.Observable
public import PhyslibAlpha.ProbabilisticTheory.StarAlgebra.Restrict
public import PhyslibAlpha.ProbabilisticTheory.StarAlgebra.SelfAdjoint
public import PhyslibAlpha.ProbabilisticTheory.StarAlgebra.Statistics
public import PhyslibAlpha.ProbabilisticTheory.StarAlgebra.Traciality
public import PhyslibAlpha.ProbabilisticTheory.State.Barycenter
public import PhyslibAlpha.ProbabilisticTheory.State.Basic
public import PhyslibAlpha.ProbabilisticTheory.State.Convex
public import PhyslibAlpha.ProbabilisticTheory.State.Discrimination
public import PhyslibAlpha.ProbabilisticTheory.State.Metric
public import PhyslibAlpha.ProbabilisticTheory.State.NormalEquivalence
public import PhyslibAlpha.ProbabilisticTheory.State.Pairing
public import PhyslibAlpha.ProbabilisticTheory.State.Preparation
public import PhyslibAlpha.ProbabilisticTheory.State.PureMeasurement
public import PhyslibAlpha.ProbabilisticTheory.State.Separation
public import PhyslibAlpha.ProbabilisticTheory.State.StateSpace
public import PhyslibAlpha.ProbabilisticTheory.State.WeightEquivalence
public import PhyslibAlpha.ProbabilisticTheory.WStarAlgebra.Basic
public import PhyslibAlpha.ProbabilisticTheory.WStarAlgebra.BoundedSesquilinearForm
public import PhyslibAlpha.ProbabilisticTheory.WStarAlgebra.Concrete
public import PhyslibAlpha.ProbabilisticTheory.WStarAlgebra.ConjSpace
public import PhyslibAlpha.ProbabilisticTheory.WStarAlgebra.Mathlib
public import PhyslibAlpha.ProbabilisticTheory.WStarAlgebra.RankOnePairing
public import PhyslibAlpha.ProbabilisticTheory.WStarAlgebra.TracePairingNorm
public import PhyslibAlpha.ProbabilisticTheory.WStarAlgebra.TracePairingSurjectivity
public import PhyslibAlpha.ProbabilisticTheory.Weight.Basic
public import PhyslibAlpha.ProbabilisticTheory.Weight.Continuous
public import PhyslibAlpha.ProbabilisticTheory.Weight.Extension
public import PhyslibAlpha.QuantumMechanics.HarmonicOscillator.LadderSystem
public import PhyslibAlpha.QuantumMechanics.HarmonicOscillator.Vacuum
public import PhyslibAlpha.QuantumMechanics.HilbertSpaces.FiniteTarget.Operators
public import PhyslibAlpha.QuantumMechanics.HilbertSpaces.FiniteTarget.Product
public import PhyslibAlpha.QuantumMechanics.HilbertSpaces.FiniteTarget.ProductState
public import PhyslibAlpha.QuantumMechanics.QuantumHarmonicOscillator
public import PhyslibAlpha.QuantumMechanics.StinespringDilation
public import PhyslibAlpha.Relativity.General.Schwarzschild.IncompressibleSphere
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.SolidCylinder
public import PhyslibAlpha.SpaceAndTime.Space.Surfaces.SolidSphere
public import PhyslibAlpha.SpaceAndTime.Space.Surfaces.SphericalCylinder
public import PhyslibAlpha.SpaceAndTime.Space.Surfaces.SphericalShell