`OAI/Geometry/EinsteinFour/`

12212 declarations, 0 contain sorry, 0 declared as axioms; 407 files

Files

ActualJacobiODEDependence.lean 5 declarations
ActualJacobiODEExistence.lean 7 declarations
ActualJacobiODEMatrix.lean 10 declarations
ActualModelIdentification.lean 5 declarations
ActualRicciContraction.lean 7 declarations
ActualSphericalMoments.lean 1 declarations
Algebra.lean 4 declarations
AngularClifford.lean 9 declarations
AngularCurvature.lean 12 declarations
AngularDerivativeMoments.lean 11 declarations
AngularEnergy.lean 3 declarations
AngularGradient.lean 8 declarations
AngularNormal.lean 14 declarations
AngularQuadratic.lean 7 declarations
AngularRotation.lean 12 declarations
AngularSixth.lean 8 declarations
AngularTrace.lean 4 declarations
AveragedRadial.lean 4 declarations
AveragedVolume.lean 2 declarations
Averages.lean 6 declarations
Balanced.lean 3 declarations
Bianchi.lean 50 declarations
BianchiCubic.lean 6 declarations
BianchiCurvature.lean 27 declarations
BianchiCurvatureProjection.lean 11 declarations
BianchiHessian.lean 16 declarations
BianchiSlices.lean 5 declarations
Boundary.lean 13 declarations
BoundedAngularMeanValue.lean 1 declarations
CP2InvolutionFixed.lean 3 declarations
CP2NonorthogonalFixed.lean 1 declarations
CP2OddOrthogonality.lean 1 declarations
CP2Overlap.lean 14 declarations
CP2PairUniqueness.lean 2 declarations
CP2UnitGeometry.lean 4 declarations
CP2WeightedBessel.lean 4 declarations
ChartConnectionTransition.lean 7 declarations
ChartCurvatureTransition.lean 8 declarations
ChartMetricNondegeneracy.lean 3 declarations
ChartMetricSmoothness.lean 7 declarations
ChartMetricTransition.lean 7 declarations
ChartVolumeDensity.lean 6 declarations
Classification.lean 1 declarations
ClassificationScaling.lean 2 declarations
CompactDomination.lean 2 declarations
ComplexPairAlignment.lean 1 declarations
ComplexProjectiveTriangle.lean 2 declarations
ConditionalUnoriented.lean 5 declarations
ConnectionPullback.lean 9 declarations
ContinuousFieldDerivative.lean 2 declarations
ContinuousRadialComparison.lean 2 declarations
CoordinateChangeCalculus.lean 6 declarations
CoordinateConnectionUniqueness.lean 1 declarations
CoordinateMetricCompatibility.lean 5 declarations
CoordinateSecondBianchi.lean 10 declarations
CotangentHamiltonian.lean 10 declarations
CotangentJacobian.lean 21 declarations
CotangentKineticEnergy.lean 4 declarations
CotangentVolume.lean 1 declarations
CoupledCasimir.lean 16 declarations
CoupledOperator.lean 15 declarations
Coupling.lean 24 declarations
CubicWeight.lean 10 declarations
CurvatureContraction.lean 22 declarations
CurvatureCoordinateSmoothness.lean 7 declarations
CurvatureFirstBianchi.lean 6 declarations
CurvatureForm.lean 8 declarations
CurvatureGreen.lean 5 declarations
CurvatureMetricSkew.lean 16 declarations
CurvatureSecondBianchi.lean 10 declarations
CurvatureTensors00.lean 16 declarations
CurvatureTensors02.lean 757 declarations
CurvatureTensors11.lean 9 declarations
Defect.lean 12 declarations
DeterminantCompression.lean 4 declarations
DirichletEndpointInvertible.lean 1 declarations
DirichletFactorization.lean 12 declarations
DirichletLeadingPositive.lean 3 declarations
DirichletMatrix.lean 18 declarations
DirichletVectorSequence.lean 4 declarations
Energy.lean 13 declarations
EuclideanHausdorffFactor.lean 4 declarations
FiniteExceptionalMeanValue.lean 1 declarations
FiniteHodgeMultiplicity.lean 3 declarations
FiniteHodgeTraceCancellation.lean 1 declarations
FiniteRadialComparison.lean 3 declarations
FlatCurvatureDirichlet.lean 5 declarations
FlatDirichletDeterminant.lean 1 declarations
FlatDirichletGreen.lean 6 declarations
FlatDirichletGreenTrace.lean 7 declarations
FlatDirichletNormalizer.lean 7 declarations
FlatDirichletThreshold.lean 3 declarations
FlatGreenDeterminant.lean 3 declarations
FlatJacobiLimit.lean 1 declarations
FlowDifferentiability.lean 6 declarations
FlowFiniteRegularity.lean 1 declarations
FlowGermUniqueness.lean 1 declarations
FlowGreen.lean 5 declarations
FlowJointDifferentiability.lean 2 declarations
FlowLocalDifferentiability.lean 1 declarations
FlowTimeReversal.lean 1 declarations
FlowVariationalExistence.lean 4 declarations
FlowVariationalRegularity.lean 1 declarations
FourDeterminantDerivative.lean 8 declarations
FourHeatAwayBound.lean 2 declarations
FourHeatCompactTimeIntegral.lean 1 declarations
FourHeatGaussian.lean 6 declarations
FourHeatGaussianApproximation.lean 7 declarations
FourHeatGaussianConvolution.lean 4 declarations
FourHeatGaussianDifferential.lean 5 declarations
FourHeatGaussianEquation.lean 2 declarations
FourHeatGaussianMoments.lean 5 declarations
FourHeatGaussianSquare.lean 2 declarations
FourHeatGaussianTimeRegularity.lean 3 declarations
FrameAverages.lean 4 declarations
FrameBundle.lean 13 declarations
FrameCurvature.lean 7 declarations
FrameCurvatureMetricSkew.lean 5 declarations
FrameEnergy.lean 3 declarations
FrameFlow.lean 9 declarations
FrameOrientation.lean 10 declarations
FrameOrientationContinuity.lean 2 declarations
FrameRegularity.lean 1 declarations
FrameRotation.lean 7 declarations
FrameVolume.lean 1 declarations
GeneralMatrixCompression.lean 64 declarations
GeodesicAverage.lean 3 declarations
GeodesicGeometry04.lean 876 declarations
GeodesicGeometry05.lean 367 declarations
GeodesicGeometry06.lean 9 declarations
GeodesicGeometry11.lean 18 declarations
GeodesicGeometry12.lean 306 declarations
GeodesicGeometry13.lean 207 declarations
GeodesicGeometry14.lean 14 declarations
GeodesicJacobiAlgebra.lean 13 declarations
GeodesicJacobiIntegralCalculus.lean 4 declarations
GeodesicJacobiSecondVariationAlgebra.lean 21 declarations
GradientCasimir.lean 16 declarations
GradientCoordinateModel.lean 41 declarations
GradientCoordinates.lean 2 declarations
GradientMixedPairing.lean 19 declarations
GradientOperator.lean 30 declarations
GradientPairing.lean 19 declarations
GradientProjection.lean 10 declarations
HVarianceApproximation.lean 33 declarations
HeatDriftTransportAlgebra.lean 3 declarations
HeatForcedScalar.lean 1 declarations
HeatKernels06.lean 1 declarations
HeatKernels10.lean 763 declarations
HeatRoughTraceAlgebra.lean 2 declarations
HessianAlgebra.lean 13 declarations
HessianAssembly.lean 15 declarations
HessianCompression.lean 22 declarations
HessianTraceEquation.lean 5 declarations
HighestAction.lean 7 declarations
HighestActionCoordinates.lean 136 declarations
HighestCondition.lean 7 declarations
HighestConstraints.lean 30 declarations
HighestCoordinates.lean 81 declarations
HighestCurvature.lean 13 declarations
HighestGram.lean 6 declarations
HighestHessian.lean 66 declarations
HighestLinear.lean 30 declarations
HighestMinus.lean 10 declarations
HighestMinusCoordinates.lean 137 declarations
HighestMinusForm.lean 9 declarations
HighestProjection.lean 25 declarations
HighestSquare.lean 16 declarations
HighestVectorSpace.lean 26 declarations
HilbertImageTotal.lean 3 declarations
HodgeTheory06.lean 33 declarations
HodgeTheory08.lean 559 declarations
HodgeTheory09.lean 237 declarations
HodgeTheory11.lean 249 declarations
InvariantGeodesic.lean 1 declarations
Jacobi.lean 8 declarations
JacobiApproximation.lean 12 declarations
JacobiAverage.lean 9 declarations
JacobiCompression.lean 8 declarations
JacobiCompressionLimit.lean 2 declarations
JacobiCurvatureCap.lean 5 declarations
JacobiCyclicPowers.lean 4 declarations
JacobiDensityMeasurability.lean 11 declarations
JacobiDeterminant.lean 2 declarations
JacobiDeterminantJensen.lean 1 declarations
JacobiDirichletLimit.lean 2 declarations
JacobiDirichletPositivity.lean 1 declarations
JacobiExpectedLog.lean 1 declarations
JacobiFiniteLower.lean 2 declarations
JacobiFullCurvatureNorm.lean 3 declarations
JacobiInverse.lean 2 declarations
JacobiKernelAverage.lean 3 declarations
JacobiKernelBound.lean 1 declarations
JacobiKernelLowerCap.lean 2 declarations
JacobiKernelPowers.lean 5 declarations
JacobiKernelTrace.lean 2 declarations
JacobiLogDetSeries.lean 6 declarations
JacobiMatrixLoss.lean 7 declarations
JacobiMeshCoefficient.lean 2 declarations
JacobiMeshError.lean 2 declarations
JacobiMeshInverse.lean 2 declarations
JacobiNearZero.lean 5 declarations
JacobiNormalized.lean 6 declarations
JacobiODELimit.lean 3 declarations
JacobiODEPositivity.lean 12 declarations
JacobiPivots.lean 7 declarations
JacobiPositivity.lean 3 declarations
JacobiPreconjugate.lean 1 declarations
JacobiRadialDeficit.lean 2 declarations
JacobiRadialODE.lean 4 declarations
JacobiRatioLimit.lean 3 declarations
JacobiRiemann.lean 3 declarations
JacobiScheme.lean 13 declarations
JacobiSchemeError.lean 1 declarations
JacobiSchemeMatrix.lean 3 declarations
JacobiSchemeRatios.lean 6 declarations
JacobiSeriesIntegral.lean 1 declarations
JacobiSineReference.lean 3 declarations
JacobiSymmetricKernel.lean 7 declarations
JacobiTraceAverage.lean 2 declarations
JacobiTraceProducts.lean 4 declarations
JacobiVolume.lean 1 declarations
JacobiWronskian.lean 8 declarations
LocalCoordinateMeasure.lean 3 declarations
LocalIncrementMeanValue.lean 1 declarations
LowerVolumeIntegral.lean 4 declarations
Matrix.lean 4 declarations
MatrixGeodesicAverage.lean 3 declarations
MatrixRatioPositivity.lean 2 declarations
MatrixSlotCompression.lean 9 declarations
MatrixSlotCubic.lean 4 declarations
MatrixSlotLaplacian.lean 2 declarations
MatrixSlotOperator.lean 20 declarations
MetricBianchi.lean 10 declarations
MetricChartDistance.lean 2 declarations
MetricChartLipschitz.lean 2 declarations
MetricChartPath.lean 1 declarations
MetricContractionCalculus.lean 3 declarations
MetricCurvatureGreen.lean 9 declarations
MetricDistance.lean 6 declarations
MetricDoubleCover.lean 12 declarations
MetricDoubleCoverModels.lean 2 declarations
MetricHessian.lean 10 declarations
MetricInverseCalculus.lean 2 declarations
MetricLinearChartPath.lean 1 declarations
MetricMatrixGreen.lean 4 declarations
MetricMinusGreen.lean 3 declarations
MetricQuadraticPerturbation.lean 3 declarations
MetricTensorCompatibility.lean 2 declarations
MinusProjectionCost.lean 13 declarations
ModeAverageLimit.lean 7 declarations
ModeCompression.lean 9 declarations
ModelIdentification.lean 2 declarations
MomentObstruction.lean 22 declarations
Moments.lean 3 declarations
NormVarianceApproximation.lean 26 declarations
OperatorGreen.lean 3 declarations
OrientationCoverCharts.lean 11 declarations
OrientationCoverClopenSheet.lean 5 declarations
OrientationCoverClosed.lean 3 declarations
OrientationCoverCompactness.lean 2 declarations
OrientationCoverCore.lean 13 declarations
OrientationCoverCurvature.lean 7 declarations
OrientationCoverDeckMetric.lean 5 declarations
OrientationCoverDistanceDown.lean 3 declarations
OrientationCoverLocalIsometry.lean 2 declarations
OrientationCoverMetric.lean 4 declarations
OrientationCoverMetricDoubleCover.lean 2 declarations
OrientationCoverPathLift.lean 3 declarations
OrientationCoverProjection.lean 4 declarations
OrientationCoverSmoothLift.lean 2 declarations
OrientationCoverTangent.lean 2 declarations
OrientationCoverTopology.lean 13 declarations
OrientationQuotient.lean 1 declarations
OrthogonalCompression.lean 5 declarations
OrthonormalFrame.lean 6 declarations
ParameterCost.lean 2 declarations
PositiveDeterminantOrder.lean 2 declarations
Potential.lean 43 declarations
ProjectionCost.lean 6 declarations
Quartic.lean 26 declarations
QuarticClosed.lean 4 declarations
QuarticEnergy.lean 6 declarations
QuaternionGenerators.lean 10 declarations
QuaternionLifts.lean 6 declarations
QuaternionReflections.lean 20 declarations
Quotient.lean 3 declarations
RadialCoefficient.lean 4 declarations
RadialIntegrals.lean 13 declarations
RationalBettiTransport.lean 3 declarations
RationalBettiZero.lean 3 declarations
RealVectorCost.lean 18 declarations
RealVectorProjection.lean 7 declarations
ReferenceCompression.lean 3 declarations
RicciGradient.lean 6 declarations
RicciMatrixChange.lean 3 declarations
RiemannianVolume.lean 8 declarations
RiemannianVolumeFinite.lean 2 declarations
RiemannianVolumePositive.lean 2 declarations
ScalarAdjointCoordinates.lean 11 declarations
ScalarAdjointTests.lean 3 declarations
ScalarBoundedBessel.lean 3 declarations
ScalarBoundedPairing.lean 4 declarations
ScalarCompactExtremal.lean 2 declarations
ScalarCompositionHessian.lean 4 declarations
ScalarContinuousLift.lean 8 declarations
ScalarDirichlet.lean 19 declarations
ScalarEigenMultiplier.lean 3 declarations
ScalarFullBallIntegerGain.lean 2 declarations
ScalarGreenLimit.lean 4 declarations
ScalarH1CompositionL2.lean 6 declarations
ScalarH1EllipticGain.lean 2 declarations
ScalarH2Closure.lean 2 declarations
ScalarH2EllipticGain.lean 1 declarations
ScalarHalfBallCutoffs.lean 14 declarations
ScalarHalfBallH2Gain.lean 1 declarations
ScalarHomogeneousInteger.lean 1 declarations
ScalarIntegerEllipticGain.lean 1 declarations
ScalarIntegrableSeries.lean 1 declarations
ScalarIterationRegularity.lean 1 declarations
ScalarL2BoundedMultiplier.lean 2 declarations
ScalarL2ClosedDomination.lean 1 declarations
ScalarL2EllipticGain.lean 1 declarations
ScalarL4ProductConvergence.lean 4 declarations
ScalarLocalHilbertSum.lean 3 declarations
ScalarLocalL2Source.lean 1 declarations
ScalarLpNormVariation.lean 6 declarations
ScalarLpRelativeVariation.lean 4 declarations
ScalarLpVariation.lean 5 declarations
ScalarMinimizingSequence.lean 2 declarations
ScalarNormalizer.lean 6 declarations
ScalarOpenIntegerEllipticGain.lean 1 declarations
ScalarPoissonKernelAdjoint.lean 8 declarations
ScalarPoissonKernelAdjointEstimate.lean 26 declarations
ScalarPoissonKernelBesselEstimate.lean 34 declarations
ScalarPoissonKernelBootstrap.lean 12 declarations
ScalarPoissonKernelCommutator.lean 8 declarations
ScalarPoissonKernelContinuousEmbedding.lean 7 declarations
ScalarPoissonKernelCutoffs.lean 16 declarations
ScalarPoissonKernelDerivative.lean 13 declarations
ScalarPoissonKernelFiniteEmbedding.lean 11 declarations
ScalarPoissonKernelHelmholtz.lean 7 declarations
ScalarPoissonKernelLocal.lean 4 declarations
ScalarPoissonKernelLocalRegularity.lean 4 declarations
ScalarPoissonKernelLocalRepresentative.lean 11 declarations
ScalarPoissonKernelLocalTests.lean 9 declarations
ScalarPoissonKernelLocalization.lean 21 declarations
ScalarPoissonKernelLocalizationChain.lean 3 declarations
ScalarPoissonKernelMeasure.lean 3 declarations
ScalarPoissonKernelMultiplier.lean 5 declarations
ScalarPoissonKernelPerturbation.lean 14 declarations
ScalarPoissonKernelPotential.lean 11 declarations
ScalarPoissonKernelSobolev.lean 10 declarations
ScalarPoissonKernelSourceChain.lean 4 declarations
ScalarPoissonKernelUniqueness.lean 10 declarations
ScalarRegularity06.lean 237 declarations
ScalarRegularity07.lean 1280 declarations
ScalarSecondDerivativeMinimum.lean 1 declarations
ScalarSpectralOrthogonal.lean 1 declarations
SineAverage.lean 17 declarations
SineEstimates.lean 9 declarations
SineLogPolynomial.lean 9 declarations
SineLogRemainder.lean 4 declarations
SineModeLimit.lean 7 declarations
Spectral.lean 2 declarations
SphericalFourthMoment.lean 6 declarations
SphericalIntegralDerivative.lean 3 declarations
SphericalMeasureCharts.lean 14 declarations
SphericalMeasureInvariance.lean 3 declarations
SphericalMeasureMass.lean 8 declarations
SphericalMomentRecurrence.lean 8 declarations
SphericalMoments.lean 14 declarations
SphericalPairMix.lean 6 declarations
SphericalRotation.lean 13 declarations
SphericalSecondMoment.lean 16 declarations
SphericalSixthMoment.lean 4 declarations
Statement.lean 2 declarations
TensorPairing.lean 16 declarations
TopologicalNumbers.lean 4 declarations
TraceAction.lean 7 declarations
TraceActionIntertwining.lean 74 declarations
TraceAdjoint.lean 18 declarations
TraceCurvature.lean 7 declarations
TraceDecomposition.lean 9 declarations
TraceGreen.lean 4 declarations
TraceHessian.lean 39 declarations
TraceSubtraction.lean 9 declarations
Variance.lean 9 declarations
VarianceCorrection.lean 1 declarations
VolumeAssembly.lean 4 declarations
VolumeConstants.lean 26 declarations
WeightedAreaInequality.lean 1 declarations
WeightedConnectionCurvature.lean 5 declarations
WeightedCost.lean 2 declarations
WeightedCurve.lean 2 declarations
WeightedHessian.lean 2 declarations
WeylDerivative.lean 13 declarations
WeylEstimates00.lean 600 declarations
WeylEstimates01.lean 952 declarations
WeylEstimates03.lean 1420 declarations
WeylEstimates06.lean 5 declarations
WeylEstimates07.lean 13 declarations
WeylEstimates14.lean 3 declarations
WeylGeometry.lean 26 declarations
WeylLaplacian.lean 9 declarations
WeylMatrixEquation.lean 12 declarations
WeylNormal.lean 9 declarations