`OAI/Geometry/PrescribedPotential/`

2070 declarations, 0 contain sorry, 0 declared as axioms; 259 files

Files

ABPIntegralBound.lean 1 declarations
AffineFamilyJets.lean 1 declarations
AnalyticSupport.lean 236 declarations
AtlasLocalization.lean 5 declarations
AugmentedVolume.lean 4 declarations
BallSubmean.lean 6 declarations
BernsteinEnergyInterior.lean 2 declarations
BernsteinHigherRescue.lean 2 declarations
BernsteinLocalC2.lean 2 declarations
BernsteinProductMaximum.lean 2 declarations
BernsteinQuarticAlgebra.lean 3 declarations
BootstrapCalculus.lean 3 declarations
BoundedBilinearCompletion.lean 7 declarations
BoundedNormalFrames.lean 8 declarations
BoundedPathContinuation.lean 4 declarations
BoundedPoisson.lean 16 declarations
CalabiBochner.lean 9 declarations
CalabiConnection.lean 12 declarations
CalabiCoordinateBound.lean 7 declarations
CalabiCoordinateCoercivity.lean 7 declarations
CalabiCovariant.lean 8 declarations
CalabiCutoffAlgebra.lean 2 declarations
CalabiCutoffFrames.lean 8 declarations
CalabiCutoffPoint.lean 1 declarations
CalabiFrameAlgebra.lean 4 declarations
CalabiFrameCalculus.lean 5 declarations
CalabiFrameScalars.lean 4 declarations
CalabiLocalUniform.lean 2 declarations
CalabiNormAlgebra.lean 12 declarations
CalabiPairCalculus.lean 8 declarations
CalabiPointInequalities.lean 6 declarations
CalabiRescue.lean 9 declarations
CalabiResidualBound.lean 11 declarations
CalabiRicciContraction.lean 6 declarations
CalabiRicciFrames.lean 6 declarations
CalabiTensorAlgebra.lean 9 declarations
ChartParametrix.lean 7 declarations
ChartTransport.lean 13 declarations
ChartTransportHigher.lean 8 declarations
ChernLuFrameInequality.lean 2 declarations
ChernLuIdentity.lean 2 declarations
ChernLuLocalInequality.lean 5 declarations
ChernLuMaximum.lean 4 declarations
CircleRadialCalculus.lean 18 declarations
CircleSubmeanCalculus.lean 1 declarations
ClosedRangeSmooth.lean 6 declarations
CommutatorSupport.lean 10 declarations
CompactAlternative.lean 1 declarations
CompactCoefficientBootstrap.lean 1 declarations
CompactHomogeneousBounds.lean 2 declarations
CompactIntegralPropagation.lean 2 declarations
CompactSmoothCutoff.lean 1 declarations
CompletedProduct.lean 5 declarations
CompletedRealification.lean 9 declarations
CompletedResolvent.lean 18 declarations
CompletedVolume.lean 4 declarations
ComplexContactDeterminant.lean 2 declarations
ComplexHessian.lean 10 declarations
ComplexKernel.lean 4 declarations
ComplexOperator.lean 14 declarations
ConstantProjection.lean 5 declarations
ContactSetABP.lean 10 declarations
CoordinateBalls.lean 12 declarations
CoordinateEllipticity.lean 4 declarations
CoordinateExtension.lean 5 declarations
CoordinateInnerCover.lean 5 declarations
CoordinateMinimumBound.lean 1 declarations
CoordinatePotential.lean 11 declarations
CoreBounds.lean 13 declarations
CutoffHigher.lean 11 declarations
DerivativeEllipticGain.lean 3 declarations
DerivativeLocalization.lean 6 declarations
DeterminantOrder.lean 3 declarations
DirectionalJetEnergy.lean 8 declarations
EncodedMetricEquation.lean 3 declarations
EvenRellich.lean 8 declarations
FamilyBernsteinBootstrap.lean 2 declarations
FiniteSobolevEmbedding.lean 3 declarations
FixedScaleBootstrap.lean 12 declarations
FourierKernel.lean 7 declarations
FrameCompactBounds.lean 8 declarations
FrameSecondCalculus.lean 3 declarations
FredholmKernel.lean 2 declarations
FredholmRegularity.lean 11 declarations
FrequencyApprox.lean 15 declarations
FrozenEllipticJets.lean 6 declarations
FrozenPoisson.lean 38 declarations
GlobalBounds.lean 9 declarations
GlobalCompletion.lean 16 declarations
GlobalConjugation.lean 13 declarations
GlobalError.lean 3 declarations
GlobalExtension.lean 9 declarations
GlobalFiniteEmbedding.lean 2 declarations
GlobalHessian.lean 7 declarations
GlobalMetricEntries.lean 12 declarations
GlobalNonlinearCommutator.lean 2 declarations
GlobalOperator.lean 10 declarations
GlobalParametrix.lean 12 declarations
GlobalParametrixEquation.lean 8 declarations
GlobalPartition.lean 13 declarations
GlobalProduct.lean 5 declarations
GlobalRellich.lean 5 declarations
GlobalSmooth.lean 12 declarations
GlobalSobolev.lean 18 declarations
GlobalStrongEmbedding.lean 7 declarations
GlobalTransport.lean 7 declarations
GradientJacobian.lean 5 declarations
HessianCommutator.lean 6 declarations
HigherDirectionalJets.lean 13 declarations
HigherJetCommutator.lean 4 declarations
HigherJetComposition.lean 4 declarations
HigherMetricOperator.lean 6 declarations
HigherPoisson.lean 7 declarations
HigherResolvent.lean 3 declarations
HolomorphicDirection.lean 4 declarations
IntegerBounds.lean 9 declarations
InverseTraceCalculus.lean 4 declarations
InverseTraceFunction.lean 8 declarations
JetDissipation.lean 7 declarations
JetEnergyCoercivity.lean 5 declarations
JetEnergyEstimates.lean 3 declarations
JetEnergyUniform.lean 7 declarations
JetNormEquivalence.lean 3 declarations
KaehlerClosedDerivatives.lean 8 declarations
KaehlerSecondDerivatives.lean 3 declarations
KernelCompact.lean 3 declarations
LinearFrameCalculus.lean 10 declarations
LinearizedCommutator.lean 10 declarations
LiteralWeakHessian.lean 12 declarations
LocalPotentialABP.lean 3 declarations
LocalRegularity.lean 50 declarations
LocalizedCompact.lean 10 declarations
LocalizedDerivations.lean 10 declarations
LocalizedPullback.lean 14 declarations
LogHessianCalculus.lean 4 declarations
MatrixCoefficientSmooth.lean 2 declarations
MatrixFrameNormalization.lean 6 declarations
MatrixHilbertCoordinates.lean 19 declarations
MatrixJetDirection.lean 8 declarations
MatrixLimit.lean 2 declarations
MatrixLogDet.lean 10 declarations
MatrixPositivity.lean 5 declarations
MatrixRealFrames.lean 8 declarations
MatrixTensorCalculus.lean 7 declarations
MatrixTraceInequalities.lean 5 declarations
MatrixWirtinger.lean 15 declarations
MetricFamilyBootstrap.lean 1 declarations
MetricInverseTrace.lean 7 declarations
MetricLocalization.lean 8 declarations
MetricQuasilinearEquation.lean 1 declarations
NonlinearCoreCommutator.lean 2 declarations
NonlinearHessianCommutator.lean 11 declarations
NonlinearLocalCoordinates.lean 5 declarations
NonlinearRemainder.lean 8 declarations
NonlinearRemainderStrong.lean 1 declarations
NonlinearScale.lean 10 declarations
NonlinearSobolevGain.lean 5 declarations
NormalizedPathCompactness.lean 3 declarations
NormalizedPoisson.lean 5 declarations
NormalizedPotentialL1.lean 2 declarations
ParameterCoreBounds.lean 6 declarations
ParameterLocal.lean 13 declarations
ParameterRegularity.lean 21 declarations
ParameterResolvent.lean 31 declarations
ParameterSchwartz.lean 8 declarations
ParametrixAtlas.lean 12 declarations
ParametrixCommutator.lean 8 declarations
PatchCutoffs.lean 7 declarations
PatchDifferential.lean 18 declarations
PathCalabiBound.lean 2 declarations
PathCalabiRicci.lean 5 declarations
PathCoordinateC1.lean 2 declarations
PathCoordinateDensity.lean 2 declarations
PathEllipticity.lean 1 declarations
PathFrameBounds.lean 1 declarations
PathLaplaceJets.lean 5 declarations
PathLaplacianSobolev.lean 2 declarations
PathMetricBootstrap.lean 3 declarations
PathMetricCompactC1.lean 3 declarations
PathPotentialBound.lean 2 declarations
PathRicci.lean 6 declarations
PathTraceBound.lean 2 declarations
PointPoisson.lean 12 declarations
PoissonEquivalence.lean 10 declarations
PositiveOpenness.lean 3 declarations
PositivePotentialLinearization.lean 4 declarations
PotentialDensity.lean 10 declarations
PotentialDensityDifferential.lean 2 declarations
PotentialLinearCalculus.lean 3 declarations
PrescribedPotential.lean 1 declarations
PrincipalComponents.lean 6 declarations
QuadraticContact.lean 4 declarations
QuantitativeResolvent.lean 7 declarations
QuasiPSHLocalMean.lean 3 declarations
QuasilinearFamilyBootstrap.lean 2 declarations
QuasilinearHighResiduals.lean 3 declarations
QuasilinearJetBasics.lean 9 declarations
QuasilinearLowResiduals.lean 4 declarations
QuasilinearResidualAlgebra.lean 3 declarations
RealCutoffBounds.lean 3 declarations
RealDeterminantOrder.lean 6 declarations
RealFrameScalar.lean 11 declarations
RealJetEnergy.lean 15 declarations
RealMapSmooth.lean 2 declarations
RealNonlinearCommutator.lean 8 declarations
RealNonlinearDerivative.lean 9 declarations
RealPoisson.lean 11 declarations
RealPoissonEquivalence.lean 3 declarations
RealSmoothCompactness.lean 4 declarations
RealSmoothOperator.lean 6 declarations
RealSobolev.lean 18 declarations
RealVolume.lean 7 declarations
RegularityCoordinates.lean 8 declarations
RegularityCutoffs.lean 11 declarations
RegularityJets.lean 12 declarations
ResidualFamilyBootstrap.lean 3 declarations
ScalarFrameCalculus.lean 7 declarations
ScalarPrincipalWirtinger.lean 4 declarations
ScalarProductLaplacian.lean 7 declarations
SchwartzConjugation.lean 6 declarations
SchwartzFamilyBounds.lean 4 declarations
SecondJetComposition.lean 3 declarations
SmoothChartInverse.lean 7 declarations
SmoothDistributions.lean 11 declarations
SmoothLocalPath.lean 3 declarations
SmoothPathLimit.lean 7 declarations
SmoothPathOpenness.lean 8 declarations
SmoothPotentialDifference.lean 5 declarations
SmoothSequenceCompactness.lean 3 declarations
SobolevDetDifferential.lean 4 declarations
SobolevDeterminant.lean 6 declarations
SobolevEmbedding.lean 11 declarations
SobolevExponential.lean 11 declarations
SobolevFirstGain.lean 4 declarations
SobolevLocalization.lean 17 declarations
SobolevOpenness.lean 3 declarations
SobolevParametrix.lean 28 declarations
SobolevProduct.lean 11 declarations
SobolevReconstruction.lean 8 declarations
SourceTarget.lean 5 declarations
StrongDerivatives.lean 8 declarations
StrongSobolevEmbedding.lean 14 declarations
SymmetricPrincipalFrame.lean 6 declarations
TraceEllipticity.lean 7 declarations
TracePositivity.lean 3 declarations
TruncatedRellich.lean 8 declarations
TwoScaleRegularity.lean 8 declarations
UniformCompositionFamily.lean 3 declarations
UniformJetControls.lean 2 declarations
UniformPathSobolev.lean 3 declarations
VariablePoisson.lean 20 declarations
VolumeDeterminantBounds.lean 2 declarations
VolumeNormalization.lean 5 declarations
VolumePath.lean 15 declarations
WeakDerivativeLocalization.lean 3 declarations
WeakNonlinearCommutator.lean 6 declarations
WeakPositive.lean 7 declarations
WirtingerCalculus.lean 16 declarations
WirtingerConjugate.lean 5 declarations