`OAI/Geometry/NodalSets/Charts/`

954 declarations, 0 contain sorry, 0 declared as axioms; 261 files

Files

AbsolutePiola.lean 4 declarations
AdaptedChartFamilyLemmas.lean 9 declarations
AdaptedMetricFrame.lean 1 declarations
AdaptedNormalChart.lean 3 declarations
AdmissibleChartPatch.lean 2 declarations
BallGeometry.lean 6 declarations
BaseChartFlux.lean 10 declarations
CenteredSphereChart.lean 7 declarations
CenteredSphereDensity.lean 4 declarations
CenteredSphereMetricLemmas.lean 6 declarations
CenteredSphereSecondJet.lean 3 declarations
ChartDerivativeTransfer.lean 3 declarations
ChartFrameSmooth.lean 7 declarations
ChartHessianLemmas.lean 10 declarations
ChartMetric.lean 6 declarations
ChartNormComparison.lean 2 declarations
ChartOperatorIdentity.lean 5 declarations
ChartPushforward.lean 6 declarations
ChartedEnvelope.lean 10 declarations
CircleChartFactor.lean 6 declarations
CircleInvariantDerivative.lean 4 declarations
CircleLaplacian.lean 1 declarations
CommonInjectiveChart.lean 4 declarations
CommonInvariantCharts.lean 1 declarations
CommonSmoothChart.lean 1 declarations
CompactFrameCover.lean 9 declarations
ComplexMetricFlux.lean 7 declarations
ContactGeometry.lean 3 declarations
ContinuousAdaptedFrame.lean 1 declarations
CorrugationFrameBounds.lean 3 declarations
CorrugationFrameOperatorBounds.lean 2 declarations
CorrugationFrameVolume.lean 1 declarations
CorrugationFrozenFrame.lean 7 declarations
CorrugationGridFrames.lean 1 declarations
CorrugationMetricError.lean 4 declarations
CorrugationMetricErrorRescale.lean 3 declarations
CorrugationRadialMetric.lean 2 declarations
CorrugationRotatingFrame.lean 9 declarations
FiniteChartDerivativeSeminorm.lean 4 declarations
FiniteChartDerivativeSize.lean 8 declarations
FixedChartAmbientLaplacian.lean 3 declarations
FixedChartRoundOperator.lean 4 declarations
FixedChartSeedEquation.lean 1 declarations
FixedChartSeedSupport.lean 3 declarations
FrameCotangent.lean 5 declarations
FrameMapFamily.lean 11 declarations
GeometricContact.lean 1 declarations
GlobalSphereEquation.lean 3 declarations
ImmersionMetric.lean 3 declarations
IndependentAmbientMetric.lean 6 declarations
IntrinsicChartTensor.lean 7 declarations
IntrinsicCorrectedChart.lean 2 declarations
IntrinsicDifferentialPairChart.lean 2 declarations
IntrinsicGlobalSphereStage.lean 1 declarations
IntrinsicLiftGeometry.lean 4 declarations
IntrinsicPackedGlobalSphereStage.lean 1 declarations
IntrinsicPackedPositiveSphereStage.lean 1 declarations
IntrinsicUniformPositiveSphereStage.lean 1 declarations
InvariantFrameInverse.lean 2 declarations
InverseChartJets.lean 3 declarations
InverseMetricJet.lean 6 declarations
LocalAdaptedFrame.lean 2 declarations
LocalFrameTriple.lean 3 declarations
LocalMetricChart.lean 2 declarations
LocalMetricJetContinuityLemmas.lean 17 declarations
LocalMetricJets.lean 4 declarations
LocalPiolaDivergence.lean 1 declarations
ManifoldCompactExtension.lean 2 declarations
ManifoldMatrixSmooth.lean 4 declarations
MatrixMetricPullback.lean 6 declarations
MetricCoercivity.lean 3 declarations
MetricConnectionFamilyLemmas.lean 8 declarations
MetricFluxPullback.lean 6 declarations
MetricFrameOps.lean 11 declarations
MetricFrequencyBounds.lean 5 declarations
MetricJetAdmissibility.lean 8 declarations
MetricNormalizationBounds.lean 3 declarations
MetricNormalizationStabilityLemmas.lean 4 declarations
NestedChartBounds.lean 4 declarations
NormalFrameContinuous.lean 5 declarations
NormalFramePhase.lean 9 declarations
NormalTaylorMetric.lean 5 declarations
PiolaFlux.lean 5 declarations
PiolaFour.lean 2 declarations
PositiveMetric.lean 5 declarations
ProductChartFlux.lean 3 declarations
ProductChartPullback.lean 7 declarations
ProductChartVolume.lean 4 declarations
QuadraticChart.lean 10 declarations
RadialMetricIdentification.lean 6 declarations
RealFiniteAtlasBallSubsequence.lean 1 declarations
RoundChartConnection.lean 8 declarations
RoundCotangentSmooth.lean 4 declarations
RoundCotangentTensor.lean 16 declarations
RoundSphereEnergyData.lean 5 declarations
SeedChartOperator.lean 6 declarations
SeedChartPrincipal.lean 6 declarations
SeedChartScalarExtension.lean 8 declarations
SeedCoordMetricRegularity.lean 3 declarations
SeedMetricNeighborhood.lean 5 declarations
SeparatedCircleDivergence.lean 3 declarations
SimplicityEnergyDensity.lean 6 declarations
SmoothBundleInverse.lean 1 declarations
SmoothInverseChart.lean 4 declarations
SphereAffineDivergenceJets.lean 5 declarations
SphereAffineFormAnnihilation.lean 1 declarations
SphereAffineNormalizedLimit.lean 1 declarations
SphereAffinePositiveInterval.lean 1 declarations
SphereAffineSimplicityCriterion.lean 1 declarations
SphereAmbientLaplacian.lean 1 declarations
SphereC1EnergyConvergence.lean 2 declarations
SphereC1IntrinsicLimit.lean 1 declarations
SphereChartArbitrarySecond.lean 2 declarations
SphereChartConformal.lean 5 declarations
SphereChartCutoffApproximation.lean 7 declarations
SphereChartCutoffWeak.lean 1 declarations
SphereChartDerivativeMap.lean 10 declarations
SphereChartDifferenceBound.lean 2 declarations
SphereChartDivergenceData.lean 7 declarations
SphereChartEllipticCompactness.lean 1 declarations
SphereChartEnergyBounds.lean 2 declarations
SphereChartFluxL2.lean 7 declarations
SphereChartL2Comparison.lean 2 declarations
SphereChartLimitGluing.lean 1 declarations
SphereChartOpenMap.lean 3 declarations
SphereChartScalarExtension.lean 4 declarations
SphereChartStrongApproximation.lean 1 declarations
SphereChartTangentTrace.lean 6 declarations
SphereChartTestFlux.lean 6 declarations
SphereChartTransition.lean 12 declarations
SphereChartUniformH1Bounds.lean 3 declarations
SphereChartValueMap.lean 6 declarations
SphereChartVolume.lean 15 declarations
SphereChartWeakDerivative.lean 1 declarations
SphereChartWeakDivergence.lean 1 declarations
SphereCompactChartTesting.lean 1 declarations
SphereCompactFluxGreen.lean 3 declarations
SphereCompletedGreenTest.lean 1 declarations
SphereContravariant.lean 3 declarations
SphereCotangentCoordinates.lean 3 declarations
SphereCovectorRestriction.lean 7 declarations
SphereDifferenceCoercivity.lean 3 declarations
SphereDifferenceTestBound.lean 1 declarations
SphereDifferenceTestEquation.lean 1 declarations
SphereDifferenceTestLiteral.lean 1 declarations
SphereDifferenceTestMaps.lean 6 declarations
SphereDifferenceTestWeak.lean 2 declarations
SphereDifferentialCoordinates.lean 6 declarations
SphereDirichletBilinear.lean 2 declarations
SphereEnergyBilinear.lean 7 declarations
SphereEnergyCompactness.lean 1 declarations
SphereEnergyCompletion.lean 12 declarations
SphereEnergyForm.lean 7 declarations
SphereEnergyFormLimit.lean 1 declarations
SphereEnergyInnerProduct.lean 4 declarations
SphereEnergyL2Compact.lean 3 declarations
SphereEnergyL2Injective.lean 3 declarations
SphereEnergyL2Map.lean 10 declarations
SphereFiniteAtlasSubsequence.lean 1 declarations
SphereFiniteChartEnergyUpper.lean 1 declarations
SphereFiniteChartL2Comparison.lean 1 declarations
SphereFiniteJetCompactness.lean 1 declarations
SphereFiniteNeighborhoodBounds.lean 2 declarations
SphereFiniteNormIndexedCompactness.lean 1 declarations
SphereFiniteNormIntrinsicCompactness.lean 1 declarations
SphereFiniteNormMixedLimit.lean 1 declarations
SphereFiniteNormQuadraticLimit.lean 2 declarations
SphereFiniteNormVariationalLimit.lean 1 declarations
SphereFiniteOrderLimitGluing.lean 1 declarations
SphereFiniteSmoothPartition.lean 1 declarations
SphereFiniteVariationalFrame.lean 2 declarations
SphereFiniteWeakJetGain.lean 1 declarations
SphereFluxDifferenceExpansion.lean 1 declarations
SphereForcingJetNeighborhood.lean 2 declarations
SphereFormPolarization.lean 4 declarations
SphereGlobalNeighborhoodCompactness.lean 1 declarations
SphereGlobalSmoothCompactness.lean 1 declarations
SphereHessianDifferenceCoercivity.lean 1 declarations
SphereHessianFluxDifference.lean 1 declarations
SphereIndexedContinuity.lean 2 declarations
SphereIndexedDivergence.lean 1 declarations
SphereIndexedFrameConsistency.lean 2 declarations
SphereIndexedGapContinuity.lean 1 declarations
SphereIndexedGapSimplicityLemmas.lean 4 declarations
SphereIndexedIntrinsic.lean 3 declarations
SphereIntegratedFormComparison.lean 1 declarations
SphereInteriorChartWeakDerivative.lean 1 declarations
SphereInteriorDifferenceBound.lean 1 declarations
SphereInteriorDifferenceL2.lean 2 declarations
SphereInteriorFluxCoercivity.lean 1 declarations
SphereInteriorGradientDifferenceBound.lean 1 declarations
SphereInteriorJetBound.lean 1 declarations
SphereInteriorLocalizedEnergy.lean 1 declarations
SphereInteriorWeakDerivativeGain.lean 1 declarations
SphereL2LocalPullback.lean 3 declarations
SphereLimitEquation.lean 3 declarations
SphereLocalLimitGluing.lean 1 declarations
SphereMeasureChartGeometry.lean 7 declarations
SphereNormalizedGlobalLimit.lean 1 declarations
SphereNormalizedSimpleUniqueness.lean 2 declarations
SphereOperatorInvariance.lean 4 declarations
SpherePositiveMargins.lean 2 declarations
SpherePositiveNormalization.lean 1 declarations
SpherePreservingEquation.lean 4 declarations
SphereReferenceMeasure.lean 6 declarations
SphereReferenceMeasureFinite.lean 6 declarations
SphereReferenceMeasureInvariance.lean 6 declarations
SphereReferenceMeasurePositive.lean 8 declarations
SphereRestrictionArbitraryHessian.lean 4 declarations
SphereSimplicity.lean 1 declarations
SphereSimplicityAnnihilation.lean 3 declarations
SphereSimplicityBump.lean 1 declarations
SphereSimplicityEnergy.lean 3 declarations
SphereSimplicityExtension.lean 1 declarations
SphereSimplicityInNeighborhood.lean 1 declarations
SphereSimplicityKernel.lean 3 declarations
SphereSimplicityKernelForm.lean 1 declarations
SphereSimplicityRigidity.lean 3 declarations
SphereSimplicitySequenceContradiction.lean 1 declarations
SphereSimplicitySquare.lean 4 declarations
SphereSmallChartPartition.lean 2 declarations
SphereSmoothFromCharts.lean 1 declarations
SphereSmoothGreenBound.lean 2 declarations
SphereSmoothGreenLocal.lean 3 declarations
SphereSmoothL2Density.lean 4 declarations
SphereSmoothVariationalStrong.lean 1 declarations
SphereSquareDifferenceTestBound.lean 1 declarations
SphereTangentTrace.lean 5 declarations
SphereThirdFluxSymmetry.lean 1 declarations
SphereTransitionFlux.lean 4 declarations
SphereTransitionFrame.lean 5 declarations
SphereTransitionScalar.lean 4 declarations
SphereTransitionTensor.lean 4 declarations
SphereUniformChartL2.lean 2 declarations
SphereUniformDensityPairingLimit.lean 2 declarations
SphereUniformEnergyRepresentative.lean 2 declarations
SphereUniformWeakJetGain.lean 1 declarations
SphereVariationalContinuousRegularity.lean 2 declarations
SphereWeakHessianSymmetry.lean 2 declarations
SphereWeakJetSuccessor.lean 1 declarations
SphereWeakThirdSymmetry.lean 1 declarations
SphereWeightedChartL2.lean 5 declarations
SphereWeightedGradientBound.lean 1 declarations
SphereWeightedL1Bound.lean 1 declarations
SphereWeightedL2.lean 7 declarations
SphereWeightedL2Infinite.lean 4 declarations
SphereWeightedNormalization.lean 3 declarations
SphereWeightedPairingLimit.lean 2 declarations
SupportedFiniteAtlasBounds.lean 5 declarations
SupportedSphereChartBounds.lean 1 declarations
TangentGramDeterminant.lean 4 declarations
TangentialMatrixInverse.lean 5 declarations
TargetChartBasis.lean 10 declarations
TargetMetricEnergy.lean 2 declarations
TargetProductChart.lean 9 declarations
TargetShortCircleArc.lean 2 declarations
TargetWarpedMetric.lean 3 declarations
TransformedDensity.lean 7 declarations
UniformInverseChartBounds.lean 1 declarations
WeightedCircleMatrix.lean 7 declarations
WeightedCircleSmooth.lean 3 declarations