`OAI/Geometry/NodalSets/Elliptic/`

1841 declarations, 0 contain sorry, 0 declared as axioms; 509 files

Files

AdmissibilityNeighborhood.lean 1 declarations
AdmissibleDirectionTriple.lean 5 declarations
AffineRescalingJets.lean 4 declarations
AmbientDerivativeDistance.lean 2 declarations
AmbientFormMatrix.lean 3 declarations
AmbientMatrixForm.lean 5 declarations
AmplitudeBounds.lean 3 declarations
AnchoredCubeBound.lean 6 declarations
AnchoredIntervalBound.lean 1 declarations
BallPacking.lean 5 declarations
BasisDivergence.lean 2 declarations
BasisLaplacian.lean 11 declarations
BasisLaplacianReindex.lean 3 declarations
CenteredRoundOperator.lean 3 declarations
CertificateSelection.lean 2 declarations
CommonLocalExtension.lean 1 declarations
CommutatorBounds.lean 10 declarations
CompactContravariantComparison.lean 2 declarations
CompactDifferentialBound.lean 3 declarations
CompactFamilyBallJetEstimate.lean 1 declarations
CompactFamilyPointwiseEstimate.lean 1 declarations
CompactFirstJetFunctionalLimit.lean 1 declarations
CompactFluxGreen.lean 2 declarations
CompactFreezing.lean 3 declarations
CompactHessianUnitBound.lean 1 declarations
CompactLocalCompositionBounds.lean 2 declarations
CompactNormalOperator.lean 6 declarations
CompactParameterDerivativeBounds.lean 1 declarations
CompactParameterEllipticityLemmas.lean 3 declarations
CompactParameterJetBounds.lean 1 declarations
CompactSignEvents.lean 5 declarations
CompactSmoothExtension.lean 3 declarations
CompactSourceOperator.lean 3 declarations
CompactSourceRepresentatives.lean 1 declarations
CompactUniformIntegralLimit.lean 1 declarations
CompactUniformProducts.lean 2 declarations
CompactWeightedDivergenceIntegral.lean 2 declarations
CompactWeightedWeakEquation.lean 2 declarations
ContactTaylor.lean 2 declarations
ContinuousPolynomialFamily.lean 13 declarations
ContravariantPullback.lean 2 declarations
CoordinateMatrixEllipticity.lean 7 declarations
CoordinateNorm.lean 6 declarations
CoordinatePartialJets.lean 5 declarations
CoordinateTransverseDisk.lean 8 declarations
CorrugationActualLowDirection.lean 1 declarations
CorrugationAdmissibleStage.lean 1 declarations
CorrugationAffineJets.lean 3 declarations
CorrugationAnnulusBoxes.lean 5 declarations
CorrugationAnnulusCell.lean 3 declarations
CorrugationAnnulusFraction.lean 1 declarations
CorrugationAnnulusPacking.lean 4 declarations
CorrugationAssembly.lean 6 declarations
CorrugationCellGain.lean 1 declarations
CorrugationClosedCell.lean 6 declarations
CorrugationClosedCubeLocality.lean 2 declarations
CorrugationCubeIntegral.lean 2 declarations
CorrugationCubeMeasure.lean 3 declarations
CorrugationCubePartition.lean 6 declarations
CorrugationCutoff.lean 2 declarations
CorrugationDirectionEvaluations.lean 5 declarations
CorrugationDiskJets.lean 8 declarations
CorrugationDiskWell.lean 13 declarations
CorrugationEnvelopeJets.lean 3 declarations
CorrugationErrorBound.lean 1 declarations
CorrugationFastLower.lean 2 declarations
CorrugationFiniteGainLemmas.lean 3 declarations
CorrugationFirstAxis.lean 3 declarations
CorrugationFixedAmplitude.lean 2 declarations
CorrugationFixedCutoff.lean 2 declarations
CorrugationFixedStage.lean 1 declarations
CorrugationFrequencyScale.lean 13 declarations
CorrugationGainStage.lean 2 declarations
CorrugationGlobalError.lean 1 declarations
CorrugationGlobalJets.lean 9 declarations
CorrugationGradientFreezing.lean 1 declarations
CorrugationGradientRates.lean 3 declarations
CorrugationGridAdmissibility.lean 1 declarations
CorrugationGridAssembly.lean 5 declarations
CorrugationGridGain.lean 1 declarations
CorrugationGridNonvanishing.lean 2 declarations
CorrugationGridProperties.lean 3 declarations
CorrugationHighAdmissibility.lean 1 declarations
CorrugationHighRegime.lean 10 declarations
CorrugationHighScalar.lean 1 declarations
CorrugationLargeSlope.lean 1 declarations
CorrugationLeadingLength.lean 5 declarations
CorrugationLeadingVector.lean 6 declarations
CorrugationLocalAdmissibility.lean 1 declarations
CorrugationLocalHessian.lean 3 declarations
CorrugationLowAdmissibility.lean 1 declarations
CorrugationLowDirection.lean 1 declarations
CorrugationLowGradient.lean 1 declarations
CorrugationLowOldMargin.lean 1 declarations
CorrugationLowRadial.lean 1 declarations
CorrugationNonvanishing.lean 1 declarations
CorrugationNormBounds.lean 5 declarations
CorrugationNormalizedGradient.lean 4 declarations
CorrugationOldData.lean 7 declarations
CorrugationOldSpeed.lean 2 declarations
CorrugationPeriodicBounds.lean 3 declarations
CorrugationPeriodicCell.lean 5 declarations
CorrugationPeriodicFlatJets.lean 4 declarations
CorrugationPeriodicJets.lean 4 declarations
CorrugationPeriodicWell.lean 5 declarations
CorrugationProjectedDirections.lean 1 declarations
CorrugationRadialJetsLemmas.lean 6 declarations
CorrugationRadialLoss.lean 1 declarations
CorrugationRegimeBounds.lean 9 declarations
CorrugationRegimeErrors.lean 1 declarations
CorrugationScaledJetsLemmas.lean 8 declarations
CorrugationSpeed.lean 1 declarations
CorrugationStrictMargin.lean 3 declarations
CorrugationUnitRegimeErrors.lean 1 declarations
CorrugationWellBound.lean 5 declarations
CorrugationWellChoice.lean 2 declarations
CorrugationWellSlope.lean 13 declarations
CubeControlExpectation.lean 4 declarations
CubeGradientBound.lean 6 declarations
CutoffAnnulus.lean 3 declarations
CutoffProduct.lean 3 declarations
DirectionTripleAlgebra.lean 6 declarations
DirectionalJet.lean 16 declarations
Divergence.lean 2 declarations
EikonalPolynomial.lean 5 declarations
EnvelopeContactJet.lean 6 declarations
EnvelopeNestedDomainsLemmas.lean 3 declarations
EnvelopeParameterAdmissibility.lean 1 declarations
EnvelopeParameterJets.lean 3 declarations
EnvelopePlacement.lean 1 declarations
EnvelopeRegion.lean 4 declarations
ExponentialIntegralSeparation.lean 1 declarations
ExteriorCorrectedEquation.lean 2 declarations
FiniteAmplitude.lean 5 declarations
FiniteBallPacking.lean 1 declarations
FiniteCertificateWeight.lean 5 declarations
FiniteCoverIntegral.lean 1 declarations
FiniteFamilyNonzeroComplement.lean 2 declarations
FiniteJetEnergy.lean 1 declarations
FiniteLinearConstraints.lean 1 declarations
FiniteLinearity.lean 9 declarations
FiniteSubsequenceSelection.lean 1 declarations
FirstJetGoodEvent.lean 7 declarations
FirstJetNonvanishing.lean 4 declarations
FirstJetSize.lean 6 declarations
FirstMomentFromSquare.lean 1 declarations
FixedDomainLiteralPacking.lean 1 declarations
FrequencyDerivativeEnergy.lean 3 declarations
FrequencyLeibniz.lean 2 declarations
FrozenPhaseLemmas.lean 5 declarations
HalfScaleLemmas.lean 7 declarations
HessianLinearTransport.lean 3 declarations
HighRegionNonvanishing.lean 1 declarations
IndependentWeightedMatrix.lean 4 declarations
IndependentWeightedSmooth.lean 3 declarations
InitialPhasePolynomial.lean 12 declarations
IntegratedSpeedGain.lean 2 declarations
IntrinsicAmbientExtension.lean 8 declarations
IntrinsicAmbientSmooth.lean 3 declarations
IntrinsicCompactWeakEquation.lean 3 declarations
IntrinsicEnergyFiniteSum.lean 1 declarations
IntrinsicEnergyIntegrable.lean 2 declarations
IntrinsicGreenTesting.lean 2 declarations
IntrinsicNoncriticalPlacement.lean 2 declarations
IntrinsicOneStep.lean 1 declarations
IntrinsicPackedQuantitativeCertificateGain.lean 1 declarations
IntrinsicPackedSelectedStage.lean 1 declarations
IntrinsicPackedSmallCorrectedStage.lean 1 declarations
IntrinsicPairUniformBounds.lean 2 declarations
IntrinsicRealCoordinates.lean 12 declarations
IntrinsicRealEllipticity.lean 3 declarations
IntrinsicRoundPerturbation.lean 8 declarations
IntrinsicRoundReference.lean 3 declarations
IntrinsicSeedPatch.lean 4 declarations
IntrinsicSeedRegularity.lean 2 declarations
IntrinsicUniformSelectedStage.lean 1 declarations
IntrinsicUniformSmallCorrectedStage.lean 1 declarations
IntrinsicWeightedLift.lean 6 declarations
InverseSquareSmallness.lean 1 declarations
JacobianCalculus.lean 7 declarations
JetNetExtension.lean 3 declarations
LiteralSeededFieldBounds.lean 1 declarations
LocalDirection.lean 2 declarations
LocalDirectionBounds.lean 1 declarations
LocalDirectionTriple.lean 1 declarations
LocalEnvelopeDomains.lean 1 declarations
LocalFirstJetNonvanishing.lean 2 declarations
LocalFrequencyLeibniz.lean 2 declarations
LocalJetAlgebra.lean 2 declarations
LocalLogJetBounds.lean 4 declarations
LocalMainLogJets.lean 1 declarations
LocalMatrixSmooth.lean 4 declarations
LocalSpatialJet.lean 5 declarations
LocalizedCorrugation.lean 10 declarations
LogJetBounds.lean 1 declarations
Logarithm.lean 5 declarations
LowRegionSeedDominance.lean 2 declarations
MainAmplitude.lean 1 declarations
MainLogJets.lean 1 declarations
NeighborhoodJetBound.lean 1 declarations
NetDecay.lean 3 declarations
NormalizedAdmissibility.lean 1 declarations
NormalizedJetBounds.lean 5 declarations
NormalizedJetPolynomialBound.lean 1 declarations
NormalizedRescaling.lean 4 declarations
OperatorAddition.lean 5 declarations
OperatorLocality.lean 3 declarations
PackingVolumeWeight.lean 1 declarations
PairedJetControl.lean 2 declarations
PartialJetGerm.lean 2 declarations
PhaseActualJet.lean 6 declarations
PhaseBounds.lean 2 declarations
PhaseContactFamily.lean 5 declarations
PhaseJet.lean 7 declarations
PlacedEnvelopeDomains.lean 3 declarations
PlacedSmoothRepresentatives.lean 4 declarations
PolynomialEvaluation.lean 11 declarations
PolynomialJet.lean 5 declarations
PositiveBilinearBound.lean 2 declarations
PositiveContravariant.lean 5 declarations
PositiveLocalExtension.lean 1 declarations
PositiveMatrixBounds.lean 4 declarations
ProductErrorJets.lean 1 declarations
ProductFlux.lean 3 declarations
QuadraticFamily.lean 10 declarations
QuadraticTaylorBound.lean 1 declarations
QuantitativeCertificateNormalization.lean 1 declarations
RadialVolumeMatrix.lean 4 declarations
RealAffinePartialJets.lean 2 declarations
RealAllWeakJetsSmooth.lean 1 declarations
RealBallCubeContainmentLemmas.lean 11 declarations
RealBallCutoffChain.lean 6 declarations
RealBallJetEstimate.lean 1 declarations
RealCarlemanCoercivity.lean 1 declarations
RealCarlemanConjugation.lean 4 declarations
RealCarlemanEstimate.lean 2 declarations
RealCarlemanLocalConditions.lean 4 declarations
RealCarlemanSupport.lean 2 declarations
RealCarlemanWeight.lean 3 declarations
RealCommutatorDerivativeBound.lean 1 declarations
RealCompactGradientMultiplier.lean 1 declarations
RealCompactH1Approximation.lean 5 declarations
RealCompactInteriorPointwise.lean 1 declarations
RealCompactL2.lean 2 declarations
RealCompactL2MapLemmas.lean 6 declarations
RealCompactL2Product.lean 1 declarations
RealCompactLipschitzFamily.lean 2 declarations
RealCompactMultiplierLemmas.lean 4 declarations
RealCompactTestDerivative.lean 1 declarations
RealCompatibleBallLimits.lean 1 declarations
RealConvexifiedPhase.lean 9 declarations
RealConvexifiedQuadraticLemmas.lean 14 declarations
RealConvolutionContraction.lean 2 declarations
RealCoordinateDerivativeNorm.lean 3 declarations
RealCoordinateDual.lean 5 declarations
RealCoordinateEllipticLemmas.lean 11 declarations
RealCountableCompactness.lean 1 declarations
RealCountableScalarCompactness.lean 1 declarations
RealCubeAverage.lean 3 declarations
RealCubeCellApproximation.lean 5 declarations
RealCubeCellDistance.lean 5 declarations
RealCubeCellPartition.lean 9 declarations
RealCubeCutoffs.lean 2 declarations
RealCubeEnergyCompactness.lean 2 declarations
RealCubeL2Control.lean 5 declarations
RealCubeL2EmbeddingLemmas.lean 9 declarations
RealCubeVarianceTensorization.lean 1 declarations
RealCutoffAbsorption.lean 4 declarations
RealCutoffBallIntegrals.lean 2 declarations
RealCutoffIntegralsLemmas.lean 9 declarations
RealCutoffWeakJetBounds.lean 1 declarations
RealCutoffWeakJets.lean 3 declarations
RealDerivativeErrorBounds.lean 6 declarations
RealDifferenceCoercivity.lean 2 declarations
RealDifferenceEnergyBound.lean 2 declarations
RealDifferenceQuotientTest.lean 10 declarations
RealDifferentiatedEquation.lean 7 declarations
RealDivergenceEnergyAE.lean 1 declarations
RealDivergenceEnergyBound.lean 1 declarations
RealDivergenceLimit.lean 2 declarations
RealEllipticLinearity.lean 3 declarations
RealEllipticLocalCompactness.lean 1 declarations
RealEllipticLocalityLemmas.lean 10 declarations
RealEllipticProducts.lean 4 declarations
RealEllipticityNeighborhood.lean 1 declarations
RealFinCubeFubini.lean 5 declarations
RealFinCubePoincare.lean 2 declarations
RealFinCubeSlices.lean 6 declarations
RealFiniteBallJetSubsequenceLemmas.lean 2 declarations
RealFiniteJetIntegrals.lean 4 declarations
RealFiniteJetSquare.lean 4 declarations
RealFiniteLocalJetLimit.lean 3 declarations
RealFinitePositiveBounds.lean 1 declarations
RealFiniteWeakJetExtension.lean 4 declarations
RealFiniteWeightedCauchy.lean 1 declarations
RealFiniteWordBounds.lean 1 declarations
RealGlobalJetCommonBound.lean 1 declarations
RealGlobalJetEmbedding.lean 1 declarations
RealGlobalL2Multiplier.lean 6 declarations
RealH1DifferenceEquation.lean 1 declarations
RealH1TestExtension.lean 3 declarations
RealHessianDifferenceCutoffsLemmas.lean 2 declarations
RealHilbertWeakLimit.lean 1 declarations
RealInhomogeneousCaccioppoli.lean 2 declarations
RealInhomogeneousPointwise.lean 1 declarations
RealInhomogeneousWeakEquation.lean 2 declarations
RealIntegralSquare.lean 1 declarations
RealInteriorDifferencePairingLemmas.lean 4 declarations
RealInteriorFluxDifference.lean 1 declarations
RealInteriorJetEstimate.lean 2 declarations
RealInteriorSquareDifferenceTest.lean 1 declarations
RealInteriorWeakAddLemmas.lean 4 declarations
RealInteriorWeakDerivative.lean 1 declarations
RealInteriorWeakProduct.lean 1 declarations
RealInteriorWeakRestrictionLemmas.lean 6 declarations
RealInteriorWeakUniqueness.lean 1 declarations
RealIntervalDerivativeControl.lean 2 declarations
RealIntervalL2Embedding.lean 2 declarations
RealIntervalPoincare.lean 1 declarations
RealJetClosedCutoff.lean 1 declarations
RealJetCutoffEstimate.lean 1 declarations
RealJetErrorBound.lean 3 declarations
RealJetErrorEquation.lean 5 declarations
RealJetErrorExpansion.lean 2 declarations
RealJetLimitDerivative.lean 3 declarations
RealJetProductExpansion.lean 7 declarations
RealJetSuccessorCutoff.lean 1 declarations
RealJetUniformDerivative.lean 2 declarations
RealL2Convolution.lean 7 declarations
RealL2DifferenceLimit.lean 6 declarations
RealL2DifferenceQuotient.lean 11 declarations
RealL2PairingRepresentatives.lean 1 declarations
RealL2PointwiseLimit.lean 1 declarations
RealL2SmoothTesting.lean 1 declarations
RealL2TranslationContinuity.lean 3 declarations
RealL2ZeroExtension.lean 8 declarations
RealLocalBallJetEstimate.lean 1 declarations
RealLocalCaccioppoli.lean 1 declarations
RealLocalCarleman.lean 1 declarations
RealLocalEquationDifferentiation.lean 1 declarations
RealLocalInteriorJetEstimate.lean 1 declarations
RealLocalJetClosedCutoff.lean 1 declarations
RealLocalJetCutoffEstimate.lean 1 declarations
RealLocalJetErrorEquation.lean 1 declarations
RealLocalJetLimits.lean 1 declarations
RealLocalJetSuccessorCutoff.lean 1 declarations
RealLocalNestedJetCutoff.lean 1 declarations
RealLocalSmoothDerivativeLemmas.lean 2 declarations
RealLocalWeakCutoff.lean 1 declarations
RealLocalWeakDifferenceBound.lean 1 declarations
RealLocalWeakDifferenceQuadratic.lean 1 declarations
RealLocalWeakJetsSmooth.lean 1 declarations
RealLocalizedDerivativeQuadratic.lean 1 declarations
RealLocalizedDifferenceIdentity.lean 3 declarations
RealMatrixEnergy.lean 10 declarations
RealMatrixEnergyProducts.lean 6 declarations
RealMatrixEntryPerturbation.lean 1 declarations
RealMatrixTransport.lean 4 declarations
RealMeanSquareDecomposition.lean 2 declarations
RealMollifierSupport.lean 5 declarations
RealNestedCutoffWeight.lean 2 declarations
RealNestedJetCutoff.lean 1 declarations
RealNestedWeakDerivative.lean 1 declarations
RealOneSidedPropagation.lean 2 declarations
RealPartialJetLinearity.lean 3 declarations
RealPartialJetLipschitz.lean 1 declarations
RealPhaseJet.lean 7 declarations
RealPositiveNestedRadii.lean 5 declarations
RealScaledCubeIntegration.lean 5 declarations
RealScaledCubePoincare.lean 3 declarations
RealSecondCommutatorBound.lean 2 declarations
RealSecondScalarBound.lean 1 declarations
RealSmoothCutoffJetBound.lean 1 declarations
RealSmoothDifferenceBound.lean 4 declarations
RealSmoothDifferenceLimit.lean 3 declarations
RealSmoothLocalCompactness.lean 1 declarations
RealSmoothWeakJetIdentification.lean 2 declarations
RealSphericalPhase.lean 4 declarations
RealSquareCutoffEnergy.lean 3 declarations
RealSquareCutoffWeakGradient.lean 5 declarations
RealSquareDifferenceEnergy.lean 1 declarations
RealSquareDifferenceTest.lean 1 declarations
RealSupportedWeakGlobal.lean 1 declarations
RealTranslatedJetEmbedding.lean 5 declarations
RealTransportDerivatives.lean 4 declarations
RealTransportQuadratic.lean 6 declarations
RealTwiceDifferentiatedEquation.lean 1 declarations
RealWeakConvolution.lean 3 declarations
RealWeakDifferenceBound.lean 2 declarations
RealWeakDivergenceDifferentiation.lean 1 declarations
RealWeakEquationRestriction.lean 1 declarations
RealWeakHessianSymmetry.lean 1 declarations
RealWeakJetConvolution.lean 1 declarations
RealWeakJetEquation.lean 2 declarations
RealWeakJetErrorBounds.lean 1 declarations
RealWeakJetForcingBounds.lean 4 declarations
RealWeakJetLeibniz.lean 5 declarations
RealWeakJetPairings.lean 7 declarations
RealWeakJetProductBound.lean 1 declarations
RealWeakJetProducts.lean 3 declarations
RealWeakSecondCommutator.lean 4 declarations
RealWeakSecondForcing.lean 2 declarations
RealWeakThirdSymmetry.lean 2 declarations
RealWeakTranslationPairing.lean 2 declarations
RealWeightedCommutator.lean 2 declarations
RealWeightedElliptic.lean 10 declarations
RealWeightedLocalDifferenceBound.lean 2 declarations
RealWeightedShift.lean 1 declarations
RealWeightedTransport.lean 9 declarations
RealZeroBallExpansion.lean 1 declarations
ReciprocalDerivativeBound.lean 1 declarations
ReciprocalFrequencyBound.lean 1 declarations
RecursiveJet.lean 14 declarations
RescaledCoordinates.lean 2 declarations
RescaledDerivativeMoments.lean 4 declarations
RescaledGradientExpectation.lean 1 declarations
RescaledHigherJets.lean 5 declarations
RescaledJetDecay.lean 3 declarations
RescaledPhase.lean 1 declarations
RescaledPhaseDefect.lean 4 declarations
RescaledSeedBounds.lean 7 declarations
RescaledSeedDecay.lean 1 declarations
RescaledSignTransfer.lean 2 declarations
RoundCoordinateGradient.lean 9 declarations
RoundDenominatorDerivatives.lean 3 declarations
RoundPerturbationFlux.lean 3 declarations
RoundQuotientBounds.lean 1 declarations
RoundReciprocalDerivatives.lean 3 declarations
RoundTensorCoordinateBounds.lean 2 declarations
ScalarBounds.lean 2 declarations
SeedAmbientHarmonic.lean 8 declarations
SeedConcretePoint.lean 10 declarations
SeedCoordAdmissibility.lean 7 declarations
SeedCoordPatchTopology.lean 8 declarations
SeedCoordinateCube.lean 6 declarations
SeedCoordinateField.lean 7 declarations
SeedDerivativeBounds.lean 2 declarations
SeedDeviationCoordinates.lean 5 declarations
SeedEnvelopePatch.lean 1 declarations
SeedFrequencyDivergence.lean 3 declarations
SeedJetLowerBound.lean 4 declarations
SeedLogConcreteJets.lean 10 declarations
SeedLogExtension.lean 8 declarations
SeedLogNonvanishing.lean 10 declarations
SeedLogSecondDerivative.lean 3 declarations
SeedLogarithmicBranch.lean 18 declarations
SeedNoncriticalPlacement.lean 2 declarations
SeedPatchTopology.lean 12 declarations
SeedPolynomialDerivatives.lean 8 declarations
SeedRadialDerivatives.lean 5 declarations
SeedRoundAdmissibility.lean 6 declarations
SeedRoundPatch.lean 9 declarations
ShiftedCenterDistance.lean 4 declarations
SignEventMarkov.lean 2 declarations
SignMass.lean 2 declarations
SignScaleContinuity.lean 6 declarations
SignScalePacking.lean 3 declarations
SignScaleSeed.lean 4 declarations
SimplicityCoordinateEnergy.lean 5 declarations
SimplicityLocalRigidity.lean 1 declarations
SimplicityRoundCoordinatePerturbation.lean 1 declarations
SmallRoundComparisonNeighborhood.lean 1 declarations
SmallRoundPerturbation.lean 4 declarations
SmoothBeamJet.lean 10 declarations
SmoothBilinearPullback.lean 3 declarations
SmoothCutoff.lean 10 declarations
SmoothDefectBounds.lean 14 declarations
SmoothJet.lean 11 declarations
SmoothOperatorJet.lean 7 declarations
SmoothQuotient.lean 4 declarations
SmoothSymmetry.lean 5 declarations
SmoothTransportJet.lean 8 declarations
SpatialJetFamily.lean 3 declarations
SpatialNet.lean 3 declarations
SphericalSeed.lean 20 declarations
StereographicArbitrarySecond.lean 2 declarations
StereographicSecondDerivative.lean 8 declarations
StrictSignSubballs.lean 2 declarations
SuccessfulTestSelection.lean 1 declarations
TargetAmbientMeasure.lean 1 declarations
TargetEmbedding.lean 6 declarations
TargetLaplacianBasis.lean 4 declarations
TargetWarpedComparison.lean 4 declarations
TargetWeightedVolume.lean 3 declarations
TaylorMatching.lean 5 declarations
TaylorPolynomial.lean 7 declarations
TransformedDrift.lean 6 declarations
TransportJet.lean 9 declarations
TransportedOperator.lean 4 declarations
TransverseCylinderVolume.lean 3 declarations
TransverseSpanning.lean 6 declarations
UniformContact.lean 4 declarations
UniformDirectional.lean 8 declarations
UniformEikonal.lean 4 declarations
UniformJets.lean 1 declarations
UniformPolynomial.lean 5 declarations
UniformRecursiveJet.lean 5 declarations
UniformSmoothBounds.lean 8 declarations
UniformSubsequenceLimit.lean 1 declarations
UniformTaylor.lean 5 declarations
UniformTransport.lean 4 declarations
UniformTransportPolynomial.lean 4 declarations
UniformTripleBounds.lean 4 declarations
WarpedAmbientForm.lean 5 declarations
WeightedCoordinateOperator.lean 4 declarations
WeightedDivergenceBounds.lean 2 declarations
WeightedDivergenceInvariance.lean 3 declarations
WeightedHessianStability.lean 3 declarations
WeightedLift.lean 6 declarations