OAI/Geometry/IsometricImmersion/Darboux/
488 declarations, 0 contain sorry, 0 declared as axioms; 52 files
Files
- ActualDriftCoefficients.lean 16 declarations
- ActualDriftEquation.lean 5 declarations
- ActualHighDrift.lean 2 declarations
- CurvaturePrincipalPart.lean 14 declarations
- DarbouxEquation.lean 3 declarations
- DarbouxJet.lean 29 declarations
- Drift.lean 4 declarations
- DriftBounds.lean 3 declarations
- DriftOperatorIdentity.lean 2 declarations
- DriftTransportAlgebra.lean 1 declarations
- HeightEquation.lean 3 declarations
- HeightPrincipalBounds.lean 10 declarations
- MixedDarbouxElimination.lean 20 declarations
- ModelPrincipal.lean 7 declarations
- QActualSegmentTransfer.lean 7 declarations
- QClosedStripMargins.lean 2 declarations
- QCoefficientTube.lean 11 declarations
- QContainingRectangle.lean 4 declarations
- QEnergyApplication.lean 8 declarations
- QFiniteActual.lean 2 declarations
- QFirstJetEnergy.lean 3 declarations
- QFirstJetFunctions.lean 33 declarations
- QFirstSpatialBounds.lean 6 declarations
- QHighEquation.lean 21 declarations
- QInitialEnergy.lean 2 declarations
- QLowActualBounds.lean 8 declarations
- QMetricDensityDecomposition.lean 8 declarations
- QMetricFirstErrorBound.lean 2 declarations
- QMetricJetTransfer.lean 4 declarations
- QMomentAbsorption.lean 4 declarations
- QPositiveFloor.lean 12 declarations
- QPrincipal.lean 10 declarations
- QReferenceInitialTolerance.lean 3 declarations
- QResidualActive.lean 6 declarations
- QResidualFactors.lean 14 declarations
- QResidualL2.lean 18 declarations
- QSameStripMargins.lean 2 declarations
- QSegmentAveraging.lean 8 declarations
- QSegmentDomain.lean 14 declarations
- QSegmentMargins.lean 5 declarations
- QSpatialFiniteInduction.lean 2 declarations
- QSpatialInductionStep.lean 1 declarations
- QSpatialJets.lean 6 declarations
- QSpatialPointwise.lean 1 declarations
- QSpatialRestriction.lean 18 declarations
- QSpatialSlabData.lean 5 declarations
- QStripJetControl.lean 5 declarations
- SixVariableDarboux.lean 28 declarations
- SixVariableLinearization.lean 11 declarations
- SixVariableQ.lean 40 declarations
- SwappedDarboux.lean 19 declarations
- TransverseCoefficient.lean 16 declarations