`OAI/Geometry/Relativity/CKS/`

4838 declarations, 0 contain sorry, 0 declared as axioms; 336 files

Files

ADMAverage.lean 12 declarations
ADMFlux.lean 9 declarations
ADMTail.lean 13 declarations
AdaptedKoszul.lean 8 declarations
AngularCoefficientBounds.lean 7 declarations
AngularCurvature.lean 9 declarations
AngularDifferentiation.lean 9 declarations
AngularFreeze.lean 5 declarations
AngularGeometry.lean 26 declarations
AngularSlice.lean 21 declarations
AngularSymbols.lean 11 declarations
AngularWeighted.lean 9 declarations
AreaCuts.lean 11 declarations
AreaGram.lean 6 declarations
BendingDerivative.lean 8 declarations
BendingFirstJet.lean 7 declarations
BendingProfiles.lean 37 declarations
BondiBalance.lean 134 declarations
BondiCharge.lean 8 declarations
BoostDivergence.lean 6 declarations
BoostFlow.lean 29 declarations
BoostIntegral.lean 11 declarations
BoostSubstitution.lean 6 declarations
BoostTransport.lean 21 declarations
BoundaryBridge.lean 10 declarations
BoundaryCharts.lean 15 declarations
BoundaryFinite.lean 3 declarations
BoundaryPartial.lean 7 declarations
BoundaryPlane.lean 4 declarations
BoundarySmooth.lean 9 declarations
CKSCoefficientRealization.lean 8 declarations
CKSCollarConcrete.lean 1 declarations
CKSCollarCoordinates.lean 7 declarations
CKSCollarExpansion.lean 4 declarations
CKSCollarSourceData.lean 4 declarations
CKSFoliationAsymptotics.lean 1 declarations
CKSFoliationFields.lean 10 declarations
CKSFoliationJet.lean 13 declarations
CKSFoliationLeading.lean 13 declarations
CKSFoliationLeadingFields.lean 12 declarations
CKSFoliationMixed.lean 2 declarations
CKSLeadingBound.lean 6 declarations
CKSLogData.lean 14 declarations
CKSMassCoefficient.lean 27 declarations
CKSMassFields.lean 22 declarations
CKSMassInputBounds.lean 6 declarations
CKSMassMixed.lean 1 declarations
CKSMetricInput.lean 8 declarations
CKSMetricPositivity.lean 8 declarations
CKSPhysicalCoefficients.lean 16 declarations
CKSPhysicalMass.lean 4 declarations
CKSPhysicalRegular.lean 8 declarations
CKSPhysicalSmooth.lean 1 declarations
CKSScaledBounds.lean 4 declarations
CKSSourceFoliationAsymptotics.lean 1 declarations
CKSSourceMass.lean 5 declarations
CKSTensorCompact.lean 6 declarations
CKSTensorFields.lean 18 declarations
CKSTensorJet.lean 33 declarations
CKSTensorMixed.lean 6 declarations
CKSTensorRealization.lean 13 declarations
ChartDistance.lean 1 declarations
CollarAngularMetric.lean 9 declarations
CollarAngularNorm.lean 7 declarations
CollarAngularWeighted.lean 10 declarations
CollarConeErrors.lean 2 declarations
CollarConstraintBounded.lean 2 declarations
CollarCutoffs.lean 10 declarations
CollarExpansionGeometry.lean 5 declarations
CollarExpansionInputNorm.lean 8 declarations
CollarExpansionJet.lean 19 declarations
CollarExpansionRealization.lean 6 declarations
CollarExpansionWeighted.lean 7 declarations
CollarFieldBounded.lean 4 declarations
CollarFieldConstraint.lean 9 declarations
CollarFieldExpansion.lean 9 declarations
CollarFieldJets.lean 18 declarations
CollarFieldLapse.lean 14 declarations
CollarFieldRegion.lean 4 declarations
CollarFieldTensor.lean 10 declarations
CollarLapseCoefficient.lean 18 declarations
CollarLapseJet.lean 17 declarations
CollarLapseRealization.lean 15 declarations
CollarLogRegular.lean 1 declarations
CollarLogSlices.lean 10 declarations
CollarMetricCoefficient.lean 14 declarations
CollarMetricComparison.lean 11 declarations
CollarMetricRealization.lean 7 declarations
CollarMomentumBounded.lean 2 declarations
CollarMomentumNormalization.lean 11 declarations
CollarMomentumWeighted.lean 5 declarations
CollarNullErrors.lean 1 declarations
CollarNullMap.lean 20 declarations
CollarNullNormalization.lean 11 declarations
CollarNullRatio.lean 7 declarations
CollarOrientation.lean 8 declarations
CollarRadialFields.lean 22 declarations
CollarRatioBounded.lean 1 declarations
CollarRawCompact.lean 12 declarations
CollarRawCurvature.lean 5 declarations
CollarRawDEC.lean 4 declarations
CollarRawFamily.lean 11 declarations
CollarRawMomentum.lean 55 declarations
CollarRawNull.lean 12 declarations
CollarRawRatio.lean 2 declarations
CollarRawSmallNull.lean 2 declarations
CollarRawWeighted.lean 3 declarations
CollarRoundReferences.lean 13 declarations
CollarShiftJet.lean 10 declarations
CollarSmallNullBounded.lean 2 declarations
CollarSourceParams.lean 2 declarations
CollarThinConstraint.lean 1 declarations
CollarThinInputs.lean 7 declarations
CollarThinInvariance.lean 8 declarations
CollarThinPrimitives.lean 26 declarations
CompactMetricCoercivity.lean 6 declarations
ComparatorDefinitions.lean 235 declarations
ComparatorMain.lean 1 declarations
ConeSupport.lean 20 declarations
ConstraintCanonical.lean 3 declarations
ConstraintCompareInterior.lean 2 declarations
ConstraintCoordinateCovariance.lean 7 declarations
ConstraintDensityDefinitions.lean 0 declarations
ConstraintGlobalIntegral.lean 2 declarations
ConstraintInterior.lean 6 declarations
ConstraintLocalInverse.lean 1 declarations
ConstraintPhysicalNormalization.lean 1 declarations
ConstraintVolumeCoordinate.lean 3 declarations
ConstructedOuterMetric.lean 864 declarations
CoordinateLeviCivita.lean 7 declarations
CovariantHeat.lean 19 declarations
CutArea.lean 4 declarations
CutAreaDefinitions.lean 0 declarations
CutSurface.lean 6 declarations
DenseInterior.lean 1 declarations
EmbeddingDerivative.lean 3 declarations
EmbeddingOpenInterior.lean 2 declarations
FoliationCurvatureOperator.lean 40 declarations
FoliationFirstJet.lean 4 declarations
FoliationFrameRegularity.lean 4 declarations
FoliationKoszul.lean 4 declarations
FoliationOrthonormalFrame.lean 7 declarations
FoliationPhysicalLeaf.lean 5 declarations
FoliationReconstruction.lean 12 declarations
FullSphereHeat.lean 9 declarations
HeatBase.lean 209 declarations
HeatChart.lean 14 declarations
HeatChartTensor.lean 9 declarations
HeatEquation.lean 11 declarations
HeatGenerated.lean 11 declarations
HeatPotential.lean 8 declarations
HeatRadial.lean 11 declarations
HeatRegularity.lean 15 declarations
HeatSymbols.lean 9 declarations
HeatTensor.lean 8 declarations
HeatUniform.lean 6 declarations
InducedMetric.lean 9 declarations
InducedSphereAlgebra.lean 45 declarations
InducedSphereCalculus.lean 38 declarations
IntrinsicEndChart.lean 2 declarations
IntrinsicReplacementDefinitions.lean 0 declarations
IntrinsicReplacementPackage.lean 1 declarations
IntrinsicReplacementWithChart.lean 1 declarations
JetBounds.lean 4 declarations
JetPolynomial.lean 17 declarations
JointJets.lean 19 declarations
LocalConstraints.lean 6 declarations
LocalMaximumHessian.lean 6 declarations
LogPhysicalCoefficients.lean 24 declarations
LogPhysicalFoliation.lean 6 declarations
LogPhysicalMass.lean 7 declarations
LogPhysicalMassJet.lean 5 declarations
LogPhysicalTensor.lean 16 declarations
LogRadialIdentity.lean 6 declarations
LogRadiusJets.lean 10 declarations
Main.lean 10 imports, no declarations
MainDefinitions.lean 2 declarations
MainProof.lean 4 declarations
MassJetRealization.lean 11 declarations
MatrixScalarJets.lean 11 declarations
MatrixThreeJets.lean 10 declarations
MeasureGlue.lean 1 declarations
MetricComparisonAssembly.lean 9 declarations
MetricPairDerivative.lean 1 declarations
MetricSymbols.lean 4 declarations
MixedCoefficientRealization.lean 7 declarations
MixedFieldJets.lean 10 declarations
MixedInputBounds.lean 12 declarations
MixedJetCalculus.lean 19 declarations
MixedJetPolynomial.lean 38 declarations
MixedMassCoefficient.lean 41 declarations
MixedMassCompact.lean 4 declarations
MixedMassFields.lean 22 declarations
MixedMassRealization.lean 10 declarations
MixedMassUniform.lean 11 declarations
MixedMatrixJets.lean 21 declarations
MixedSqrtJet.lean 3 declarations
MixedThreeJets.lean 16 declarations
NonroundConstraints.lean 21 declarations
NonroundFrame.lean 19 declarations
NonroundMass.lean 10 declarations
OriginalMetricEstimate.lean 6 declarations
OuterBounds.lean 4 declarations
OuterMetricComparison.lean 9 declarations
OuterRealization.lean 2 declarations
PhysicalAccelerationNorm.lean 2 declarations
PhysicalConnectionRegularity.lean 7 declarations
PhysicalCovariantTensor.lean 7 declarations
PhysicalCurvatureOperator.lean 8 declarations
PhysicalFoliationConstraints.lean 1 declarations
PhysicalFrameBasis.lean 4 declarations
PhysicalFrameCalculus.lean 9 declarations
PhysicalFrameConnection.lean 9 declarations
PhysicalFrameContractions.lean 7 declarations
PhysicalFrameCurvature.lean 9 declarations
PhysicalFrameTensor.lean 14 declarations
PhysicalLeafConnection.lean 8 declarations
PhysicalLeafTrace.lean 5 declarations
PhysicalMomentumCoordinate.lean 5 declarations
PhysicalMomentumCovector.lean 10 declarations
PhysicalMomentumNorm.lean 3 declarations
PhysicalNormalFrame.lean 6 declarations
RadialPrimitive.lean 10 declarations
RadialProfiles.lean 23 declarations
RadialTail.lean 7 declarations
RiemannianContraction.lean 2 declarations
RoundCasimir.lean 5 declarations
RoundReferenceJets.lean 13 declarations
ScalarJetCalculus.lean 12 declarations
ScalarThreeJets.lean 16 declarations
ScaledJetOutput.lean 2 declarations
ScaledPullback.lean 13 declarations
ScaledThreeJetOutput.lean 2 declarations
SchwarzschildAdvancedTime.lean 9 declarations
SchwarzschildArea.lean 6 declarations
SchwarzschildAreaDefinitions.lean 1 declarations
SchwarzschildBoundary.lean 8 declarations
SchwarzschildCKS.lean 13 declarations
SchwarzschildCKSAlgebra.lean 10 declarations
SchwarzschildCKSDecay.lean 9 declarations
SchwarzschildCartesianDerivatives.lean 5 declarations
SchwarzschildCharges.lean 5 declarations
SchwarzschildCharts.lean 5 declarations
SchwarzschildCompleteness.lean 8 declarations
SchwarzschildConnection.lean 9 declarations
SchwarzschildConnectionDefinitions.lean 5 declarations
SchwarzschildCoordinates.lean 13 declarations
SchwarzschildEnd.lean 12 declarations
SchwarzschildEquality.lean 5 declarations
SchwarzschildEqualityDefinitions.lean 1 declarations
SchwarzschildGraphSecondForm.lean 7 declarations
SchwarzschildHorizon.lean 4 declarations
SchwarzschildHorizonExclusion.lean 3 declarations
SchwarzschildHorizonExclusionDefinitions.lean 7 declarations
SchwarzschildIntrinsicEquality.lean 4 declarations
SchwarzschildIntrinsicHorizonDefinitions.lean 5 declarations
SchwarzschildMetric.lean 19 declarations
SchwarzschildMetricDefinitions.lean 0 declarations
SchwarzschildModel.lean 11 declarations
SchwarzschildNormalDerivative.lean 2 declarations
SchwarzschildOrientability.lean 5 declarations
SchwarzschildPosition.lean 14 declarations
SchwarzschildProfile.lean 11 declarations
SchwarzschildProjection.lean 1 declarations
SchwarzschildRadialDecay.lean 2 declarations
SchwarzschildRoundMetric.lean 8 declarations
SchwarzschildSpacetimeAlgebra.lean 8 declarations
SchwarzschildSpacetimeDefinitions.lean 0 declarations
SchwarzschildSpacetimeDerivatives.lean 5 declarations
SchwarzschildSpacetimeRegular.lean 7 declarations
SchwarzschildSpherical.lean 6 declarations
SchwarzschildStrongEquality.lean 1 declarations
SchwarzschildVacuum.lean 2 declarations
SchwarzschildVacuumRound.lean 1 declarations
SchwarzschildVacuumSpherical.lean 1 declarations
SmoothOuterDEC.lean 155 declarations
SourceBalancedChart.lean 1 declarations
SourceBalancedPatches.lean 4 declarations
SourceCollarBound.lean 3 declarations
SourceCollarMetric.lean 2 declarations
SourceExteriorDefinitions.lean 0 declarations
SourceFoliationLeading.lean 12 declarations
SourceGeometry.lean 3 declarations
SourceMassRegularity.lean 6 declarations
SourcePhysicalFoliation.lean 9 declarations
SourcePhysicalMass.lean 15 declarations
SourcePhysicalTensor.lean 16 declarations
SourceReconstruction.lean 4 declarations
SourceReplacement.lean 1 declarations
SourceReplacementDefinitions.lean 1 declarations
SourceTopology.lean 0 declarations
SphereConeAlgebra.lean 5 declarations
SphereConeChart.lean 10 declarations
SphereConeMeasure.lean 5 declarations
SphereHeat.lean 22 declarations
SphereVolume.lean 4 declarations
SphericalCharts.lean 14 declarations
SphericalDivergence.lean 5 declarations
SphericalFrame.lean 14 declarations
SphericalLaplacian.lean 8 declarations
SphericalTensor.lean 18 declarations
SphericalTensorChart.lean 10 declarations
SphericalTensorIdentity.lean 3 declarations
SurfaceBarrier.lean 4 declarations
SurfaceChristoffel.lean 5 declarations
SurfaceDeterminant.lean 2 declarations
SurfaceDivergence.lean 5 declarations
SurfaceFrames.lean 6 declarations
SurfaceImage.lean 1 declarations
SurfaceImageMeasure.lean 4 declarations
SurfaceLocalImage.lean 2 declarations
SurfaceMapDerivative.lean 8 declarations
SurfaceNormal.lean 3 declarations
SurfaceNormalization.lean 1 declarations
SurfaceParameter.lean 4 declarations
SurfaceScaling.lean 4 declarations
SurfaceVolume.lean 32 declarations
SurfaceVolumeGlobalLower.lean 2 declarations
SurfaceVolumeLower.lean 5 declarations
TailConstraints.lean 5 declarations
TailDifferentiation.lean 19 declarations
TailEnergy.lean 389 declarations
TailSymbols.lean 33 declarations
TailTensor.lean 5 declarations
Transfer.lean 7 declarations
TransferDefinitions.lean 6 declarations
VolumeAlgebra.lean 4 declarations
VolumeCompatibility.lean 3 declarations
VolumeCoordinate.lean 14 declarations
VolumeDefinitions.lean 0 declarations
VolumeExistence.lean 4 declarations
VolumeMeasurable.lean 4 declarations
VolumeRegularity.lean 4 declarations
VolumeTransition.lean 6 declarations
VolumeUnique.lean 5 declarations
WeightedArea.lean 3 declarations