`OAI/Geometry/RCD/Sobolev/`

1358 declarations, 0 contain sorry, 0 declared as axioms; 708 files

Files

ACDerivativeEndpointBound.lean 1 declarations
ActualEulerLimit.lean 1 declarations
ActualPoissonCommutator.lean 1 declarations
ActualPoissonCommutatorSpan.lean 1 declarations
ActualPoissonDifference.lean 1 declarations
ActualPoissonEulerForcing.lean 1 declarations
ActualPoissonEulerGradient.lean 1 declarations
ActualPoissonMass.lean 3 declarations
ActualPoissonQuadratic.lean 3 declarations
ActualRadialEnergy.lean 1 declarations
AffineCoefficientEnergy.lean 1 declarations
AlmostMonotoneUniformLimit.lean 1 declarations
AnnularLipschitzCutoff.lean 1 declarations
AnnularPoincare.lean 3 declarations
AveragedCutoffError.lean 3 declarations
BalancedSourceGradient.lean 3 declarations
BochnerCauchySchwarz.lean 1 declarations
BochnerCurvatureDensity.lean 2 declarations
BochnerCutoffFlux.lean 2 declarations
BochnerCutoffIdentity.lean 2 declarations
BochnerDensityQuadratic.lean 1 declarations
BochnerDensityShiftedQuadratic.lean 1 declarations
BochnerDriftProduct.lean 3 declarations
BochnerEnergyAbsorption.lean 2 declarations
BochnerGramSource.lean 5 declarations
BochnerMassComparison.lean 2 declarations
BochnerMassEstimate.lean 2 declarations
BochnerMassExponential.lean 1 declarations
BochnerMassFromEnergy.lean 2 declarations
BochnerMeasureFromSource.lean 1 declarations
BochnerMeasureIdentity.lean 1 declarations
BochnerMeasurePolarization.lean 1 declarations
BochnerMeasureProduct.lean 1 declarations
BochnerMeasureProductLocal.lean 1 declarations
BochnerMixedRecovery.lean 2 declarations
BochnerMixedTerm.lean 1 declarations
BochnerProductDensity.lean 3 declarations
BochnerQuadraticBound.lean 3 declarations
BochnerRadonDensity.lean 5 declarations
BochnerShiftedQuadratic.lean 2 declarations
BochnerSobolevLimit.lean 1 declarations
BochnerSourceFunctionals.lean 2 declarations
BochnerSourceLocality.lean 1 declarations
BochnerSourceSquare.lean 2 declarations
BochnerSourceUniqueness.lean 2 declarations
BochnerSquareSaturation.lean 2 declarations
BochnerTestForm.lean 4 declarations
BochnerWeakSubsolution.lean 1 declarations
BoundaryDirichletLayer.lean 1 declarations
BoundaryDirichletLocal.lean 1 declarations
BoundaryMaximum.lean 3 declarations
BoundaryTorsionProfile.lean 9 declarations
BoundedDyadicScale.lean 1 declarations
BoundedEnergyDensity.lean 1 declarations
BoundedEnergyIntegrableWeight.lean 1 declarations
BoundedGlobalBochner.lean 1 declarations
BoundedGlobalDimensionalBochner.lean 1 declarations
BoundedGradientLipschitz.lean 2 declarations
BoundedHarmonicScaledEnergy.lean 1 declarations
BoundedHessianApproximationIndependence.lean 1 declarations
BoundedHilbertImageWeak.lean 2 declarations
BoundedL2Difference.lean 1 declarations
BoundedLipschitzMultiplier.lean 3 declarations
BoundedLipschitzProduct.lean 2 declarations
BoundedLocalBochner.lean 1 declarations
BoundedLocalDimensionalBochner.lean 1 declarations
BoundedLocalRepresentative.lean 1 declarations
BoundedLpSquare.lean 4 declarations
BoundedPoissonLipschitz.lean 2 declarations
BoundedPositiveTail.lean 2 declarations
BoundedPowerPairContinuity.lean 3 declarations
BoundedSetTestError.lean 1 declarations
BoundedSquareLaplacian.lean 1 declarations
BoundedSquareVariation.lean 2 declarations
BoundedTestCutoffError.lean 1 declarations
BoundedTransverseTest.lean 2 declarations
BoundedWeightIntegralLimit.lean 1 declarations
CanonicalHessianApproximation.lean 1 declarations
CanonicalHessianConstantShift.lean 1 declarations
CanonicalHessianInnerPairing.lean 1 declarations
CanonicalHessianLocality.lean 1 declarations
CanonicalHessianMassBound.lean 1 declarations
CanonicalHessianRestriction.lean 1 declarations
CenteredAffineSobolev.lean 3 declarations
CenteredHarmonicEnergy.lean 1 declarations
CenteredPoissonPinching.lean 2 declarations
ClippedPositivePower.lean 2 declarations
CoerciveOpenMapping.lean 2 declarations
CoerciveQuadraticEnvelope.lean 1 declarations
ColumnGradientValueBound.lean 1 declarations
CompactBadAverage.lean 1 declarations
CompactBochnerSobolevMeasure.lean 1 declarations
CompactBochnerTest.lean 2 declarations
CompactBoundaryLayerSequence.lean 2 declarations
CompactCoerciveTruncation.lean 1 declarations
CompactCoreEnergyExtension.lean 1 declarations
CompactCutoffSource.lean 4 declarations
CompactEnergyDensity.lean 1 declarations
CompactEnergyHarmonic.lean 1 declarations
CompactFactorScaledEnergy.lean 1 declarations
CompactGradientRepresentative.lean 1 declarations
CompactIntegralDerivative.lean 1 declarations
CompactLaplacian.lean 1 declarations
CompactLipschitzLocalization.lean 1 declarations
CompactLipschitzSobolevBound.lean 1 declarations
CompactLipschitzTests.lean 7 declarations
CompactMeasureLaplacian.lean 3 declarations
CompactMixedEnergy.lean 1 declarations
CompactPointedTestRecovery.lean 3 declarations
CompactPoissonHessian.lean 2 declarations
CompactReciprocalMultiplier.lean 1 declarations
CompactRecoveryGlobalBounds.lean 1 declarations
CompactRecoveryMixedEnergy.lean 1 declarations
CompactRestrictedLaw.lean 2 declarations
CompactScalarPrimitive.lean 1 declarations
CompactSobolevTests.lean 5 declarations
CompactTestHarmonicLimits.lean 2 declarations
CompactTestHarmonicReplacements.lean 1 declarations
CompactTestPairing.lean 10 declarations
CompactTimeWeakEquation.lean 1 declarations
CompactTorsionMassBound.lean 2 declarations
ComposedGammaContinuity.lean 1 declarations
ComposedGammaPairingVariation.lean 1 declarations
ComposedGammaVariation.lean 1 declarations
ConditionalSelfPair.lean 4 declarations
ConstantLaplacianBochnerInput.lean 9 declarations
ConstantLaplacianBochnerTest.lean 2 declarations
ConstantSourceBochnerLimit.lean 2 declarations
ConstantSourceCancellation.lean 1 declarations
ContainingMassCutoffDifference.lean 1 declarations
ContainingMassCutoffErrors.lean 2 declarations
ContainingMassPoissonComparison.lean 1 declarations
ContinuousAEEqOnTime.lean 1 declarations
ContinuousDensityTestRigidity.lean 2 declarations
ContinuousDifferenceSpace.lean 10 declarations
ContinuousLocalGradientBound.lean 2 declarations
ContinuousPathMean.lean 2 declarations
ContinuousSobolevPairingBound.lean 2 declarations
ContinuousSobolevTestOrder.lean 1 declarations
ContinuousTimeCylinders.lean 1 declarations
ConvexDifferenceSpace.lean 2 declarations
ConvexSubprobability.lean 1 declarations
CorrectionInteriorEnergy.lean 3 declarations
CountableCompactDomains.lean 1 declarations
CountableLipschitzCompactness.lean 2 declarations
CoveredCoercivity.lean 1 declarations
CurvedCanonicalHessianMass.lean 1 declarations
CurvedCanonicalShiftedHessian.lean 1 declarations
CutoffBochnerConvergence.lean 2 declarations
CutoffDifferenceEnergy.lean 1 declarations
CutoffEnergyBound.lean 2 declarations
CutoffEnergyCoreConvergence.lean 1 declarations
CutoffErrorEstimates.lean 4 declarations
CutoffErrorL1.lean 1 declarations
CutoffErrorLocalization.lean 3 declarations
CutoffGamma.lean 1 declarations
CutoffGaugeEnergy.lean 1 declarations
CutoffIntegralLimit.lean 3 declarations
CutoffLevelVariation.lean 3 declarations
CutoffLocalEnergyBound.lean 1 declarations
CutoffPointwiseGradient.lean 1 declarations
CutoffPoissonLaplacian.lean 1 declarations
CutoffPoissonRepresentative.lean 1 declarations
CutoffProductEnergy.lean 1 declarations
CutoffSourcePairing.lean 2 declarations
DenseCoreGradientBound.lean 1 declarations
DenseLipschitzUniformLimit.lean 1 declarations
DenseTimeSequence.lean 1 declarations
DifferentiableMeanRemainder.lean 1 declarations
DimensionalBochnerLimit.lean 1 declarations
DimensionalBochnerTest.lean 4 declarations
DimensionalCutoffLimit.lean 2 declarations
DirectionalGradientBound.lean 2 declarations
DirichletContractions.lean 4 declarations
DirichletMaximum.lean 2 declarations
DirichletPoincare.lean 4 declarations
DirichletPoisson.lean 8 declarations
DirichletSobolevConstruction.lean 2 declarations
DirichletSobolevInput.lean 1 declarations
DirichletTail.lean 1 declarations
DirichletTestRecoverySequence.lean 3 declarations
DistanceLaplacian.lean 1 declarations
DistanceLaplacianInput.lean 2 declarations
DistancePoissonAbsoluteValues.lean 1 declarations
DistancePoissonBoundedMean.lean 1 declarations
DistancePoissonBudget.lean 2 declarations
DistancePoissonConstruction.lean 2 declarations
DistancePoissonDistanceValues.lean 2 declarations
DistancePoissonErrors.lean 3 declarations
DistancePoissonExtensions.lean 1 declarations
DistancePoissonFamily.lean 3 declarations
DistancePoissonGradient.lean 2 declarations
DistancePoissonLocalData.lean 1 declarations
DistancePoissonMeanData.lean 5 declarations
DistancePoissonMeanEstimate.lean 1 declarations
DistancePoissonRepresentative.lean 3 declarations
DistancePoissonValueL1.lean 1 declarations
DominatedTestConvergence.lean 2 declarations
DyadicBochnerMass.lean 7 declarations
DyadicBochnerSmallness.lean 1 declarations
DyadicPoissonL2Limit.lean 2 declarations
DyadicPoissonValueError.lean 1 declarations
DyadicRadialEnergy.lean 1 declarations
DyadicScalarBackground.lean 2 declarations
DyadicSubsolutionLevels.lean 1 declarations
DyadicSupportCoercivity.lean 1 declarations
DyadicTailBound.lean 1 declarations
EndpointLIntegralLimit.lean 2 declarations
EnergyAffineRigidity.lean 1 declarations
EnergyDensityLimits.lean 2 declarations
EnergyGapLimit.lean 2 declarations
EuclideanBoundedHessian.lean 1 declarations
EuclideanConstantEnergyRigidity.lean 4 declarations
EuclideanConvolutionLaplacian.lean 2 declarations
EuclideanDirectionalLaplacian.lean 2 declarations
EuclideanEnergyDifferentiation.lean 1 declarations
EuclideanEnergyRatios.lean 3 declarations
EuclideanEulerPairing.lean 2 declarations
EuclideanHarmonicHessianConstruction.lean 1 declarations
EuclideanInteriorTorsion.lean 5 declarations
EuclideanLaplacianDilation.lean 2 declarations
EuclideanLawLocalizedTests.lean 3 declarations
EuclideanLocalEnergyRigidity.lean 1 declarations
EuclideanQuadraticEnergy.lean 1 declarations
EuclideanReflectedLaplacian.lean 2 declarations
EuclideanScalarLaplacian.lean 2 declarations
EuclideanWeakHarmonicMean.lean 1 declarations
EuclideanWeakHarmonicSmooth.lean 2 declarations
EuclideanWeakHarmonicSmoothing.lean 2 declarations
EulerCoefficientSubsequence.lean 1 declarations
EulerForcing.lean 1 declarations
EulerOrthogonality.lean 3 declarations
EulerPairingLimit.lean 2 declarations
EulerRigidity.lean 6 declarations
EventualDiagonalLevel.lean 1 declarations
EverySubsequenceEventual.lean 1 declarations
ExhaustingLipschitzLimits.lean 1 declarations
ExponentialSobolev.lean 3 declarations
FiniteColumnEnergy.lean 5 declarations
FiniteDimensionalBochnerAE.lean 3 declarations
FiniteDirectedCut.lean 5 declarations
FiniteDisjointIntegral.lean 1 declarations
FiniteDominatedCurveLimit.lean 2 declarations
FiniteEnergyRepresentatives.lean 4 declarations
FiniteMeasureCompactLipschitzDensity.lean 1 declarations
FiniteMomentConvergence.lean 3 declarations
FiniteScaleCutoffBudget.lean 4 declarations
FiniteSpanOfIndependentBound.lean 1 declarations
FirstOrderTestMetricDefect.lean 1 declarations
FixedCutoffNeighborhood.lean 1 declarations
FullBochnerCutoffIdentity.lean 3 declarations
FullBochnerMassBound.lean 5 declarations
GammaColumnMixed.lean 1 declarations
GammaL2Bound.lean 3 declarations
GammaL2ContinuousAt.lean 1 declarations
GammaL2Stability.lean 2 declarations
GammaLpNorm.lean 1 declarations
GammaSquareDifference.lean 1 declarations
GeometricMeanBootstrap.lean 1 declarations
GeometricMeanSum.lean 1 declarations
GeometricMomentPointwiseBound.lean 1 declarations
GeometricTailMoment.lean 1 declarations
GoodCutoffFromResolvent.lean 5 declarations
GoodLaplacianCutoff.lean 5 declarations
GoodTimeExtension.lean 3 declarations
GradientEnergyFromDensity.lean 1 declarations
GradientProductAction.lean 3 declarations
GradientProductInput.lean 1 declarations
GradientQuadraticEnergy.lean 1 declarations
HamiltonJacobiTimeBound.lean 2 declarations
HamiltonJacobiWeakEnergy.lean 2 declarations
HarmonicBarrierTest.lean 1 declarations
HarmonicBochnerConstruction.lean 2 declarations
HarmonicBochnerCutoffLimit.lean 3 declarations
HarmonicBochnerFromHessian.lean 3 declarations
HarmonicBochnerMass.lean 1 declarations
HarmonicCoreBochnerMeasure.lean 1 declarations
HarmonicCutoffErrorBounds.lean 2 declarations
HarmonicCutoffErrorIntegral.lean 1 declarations
HarmonicCutoffMassBound.lean 2 declarations
HarmonicCutoffSwap.lean 2 declarations
HarmonicEnergyBound.lean 1 declarations
HarmonicEnergyCompactness.lean 1 declarations
HarmonicEnergyGradient.lean 1 declarations
HarmonicEnergyIdentification.lean 1 declarations
HarmonicEnergyRigidity.lean 2 declarations
HarmonicEnergyTailBound.lean 1 declarations
HarmonicEnergyTailCover.lean 1 declarations
HarmonicEnergyTailSequence.lean 1 declarations
HarmonicGradientConstruction.lean 2 declarations
HarmonicGradientFromPoisson.lean 4 declarations
HarmonicGradientInput.lean 1 declarations
HarmonicGramEnergyDefect.lean 1 declarations
HarmonicInteriorEnergy.lean 1 declarations
HarmonicL1GradientBound.lean 2 declarations
HarmonicLinearEnergyL1.lean 1 declarations
HarmonicReplacementEnergy.lean 3 declarations
HarmonicScaledEnergy.lean 1 declarations
HarmonicSequenceEnergy.lean 1 declarations
HarmonicSquareTestPositive.lean 1 declarations
HarmonicValueTestCompactness.lean 1 declarations
HarmonicWeightedEnergyLimit.lean 1 declarations
HessianActionChain.lean 2 declarations
HessianActionCoreIntegral.lean 3 declarations
HessianActionInput.lean 1 declarations
HessianActionIntegral.lean 3 declarations
HessianActionLocality.lean 2 declarations
HessianActionProduct.lean 1 declarations
HessianActionRepresentatives.lean 1 declarations
HessianCommutatorEnergy.lean 1 declarations
HessianDensityMassBound.lean 3 declarations
HessianDifferencePolarization.lean 3 declarations
HessianL1LimitUniqueness.lean 3 declarations
HessianL1MassBound.lean 2 declarations
HessianLaplacianPairing.lean 1 declarations
HessianLocality.lean 3 declarations
HessianPotentialProduct.lean 1 declarations
HessianPotentialSquare.lean 1 declarations
HessianScaledVelocity.lean 3 declarations
HessianSpanCommutator.lean 2 declarations
HessianSquareCross.lean 1 declarations
HessianVelocityPolarization.lean 3 declarations
InhomogeneousSobolev.lean 2 declarations
InnerBallCutoffSequence.lean 2 declarations
InnerBallMeasuredTests.lean 2 declarations
InnerProductVariation.lean 1 declarations
InteriorBoundedGradientRepresentative.lean 1 declarations
InteriorLipschitzTestProduct.lean 1 declarations
InteriorSmoothTestBounds.lean 1 declarations
InteriorTorsionBounds.lean 3 declarations
InteriorTorsionLaplacian.lean 1 declarations
InteriorTorsionLayer.lean 1 declarations
IntervalEnergyWeightLimit.lean 2 declarations
L1DifferenceLimit.lean 2 declarations
L1LimitLocalization.lean 2 declarations
LeftDerivativeIntegral.lean 1 declarations
LeftQuotientDerivative.lean 1 declarations
LevelSetHolderStep.lean 2 declarations
LevelTruncation.lean 8 declarations
LipschitzCompactSubsequence.lean 2 declarations
LipschitzDerivativeLimit.lean 1 declarations
LipschitzDerivativeValueLimit.lean 2 declarations
LipschitzDirectionalIntegral.lean 2 declarations
LipschitzGreenPairing.lean 1 declarations
LipschitzGreenTrace.lean 2 declarations
LipschitzL2PointControl.lean 1 declarations
LipschitzMeasureOrder.lean 2 declarations
LipschitzMetricTransfer.lean 1 declarations
LocalAffineCutoff.lean 2 declarations
LocalAverageRepresentative.lean 1 declarations
LocalBochnerDensityProduct.lean 1 declarations
LocalBochnerInput.lean 3 declarations
LocalCutoffLipschitz.lean 2 declarations
LocalEnergyMap.lean 1 declarations
LocalEnergyMeasure.lean 5 declarations
LocalGradientBoundedness.lean 2 declarations
LocalGradientDifferenceRepresentative.lean 2 declarations
LocalGradientLipschitz.lean 1 declarations
LocalGradientRepresentative.lean 2 declarations
LocalHessianAction.lean 2 declarations
LocalHessianLimitPairing.lean 1 declarations
LocalHolderMoment.lean 2 declarations
LocalL1WeakPairing.lean 1 declarations
LocalLaplacianMass.lean 1 declarations
LocalLipschitzAverages.lean 1 declarations
LocalLipschitzDenseCauchy.lean 2 declarations
LocalLipschitzDerivative.lean 1 declarations
LocalLipschitzGreenPairing.lean 1 declarations
LocalLipschitzGreenTrace.lean 2 declarations
LocalMeanEnergyFactor.lean 1 declarations
LocalMedian.lean 1 declarations
LocalMixedSourceIdentity.lean 1 declarations
LocalPoissonCompactExtension.lean 1 declarations
LocalPoissonDimensionalDensity.lean 2 declarations
LocalPoissonEnergyDensity.lean 2 declarations
LocalPoissonFullBochnerMeasure.lean 1 declarations
LocalPoissonGradientMeasure.lean 2 declarations
LocalPoissonGradientTest.lean 1 declarations
LocalPoissonHessianPairing.lean 1 declarations
LocalPoissonMeasureLaplacian.lean 2 declarations
LocalPoissonMixedShifted.lean 1 declarations
LocalPoissonPairingBound.lean 1 declarations
LocalPoissonShiftedHessian.lean 1 declarations
LocalProbabilityEnergy.lean 2 declarations
LocalProbabilityGammaBound.lean 1 declarations
LocalRepresentativeGradient.lean 1 declarations
LocalScaledGammaDifference.lean 1 declarations
LocalScaledGammaL1.lean 1 declarations
LocalScaledGammaL2.lean 1 declarations
LocalSlopeEventualBound.lean 1 declarations
LocalSlopeRateLimit.lean 1 declarations
LocalSourceStrongGradient.lean 1 declarations
LocalWeakMaximal.lean 1 declarations
LocalWeakSourceUniqueness.lean 1 declarations
LocalZeroSetCoercivity.lean 2 declarations
LocalizedCutoffNorms.lean 2 declarations
LocalizedGradientPair.lean 2 declarations
LocalizedPoissonAverages.lean 1 declarations
LocalizedPoissonRepresentative.lean 1 declarations
LogDensityGradient.lean 3 declarations
LogSumExpIntegrable.lean 3 declarations
LogSumExpIntegral.lean 2 declarations
MeanGradient.lean 5 declarations
MeanPoincareInput.lean 1 declarations
MeasureLaplacianAlgebra.lean 3 declarations
MeasureLaplacianProduct.lean 5 declarations
MeasureLaplacianUniqueness.lean 1 declarations
MeasureProductEnergy.lean 4 declarations
MeasuredLawTestBound.lean 1 declarations
MeasuredRadialCutoff.lean 3 declarations
MeasuredRadialCutoffSupport.lean 1 declarations
MeasuredSmoothTestLimits.lean 3 declarations
MeasuredTestScaling.lean 2 declarations
MedianLevel.lean 1 declarations
MetricCoercivity.lean 10 declarations
MovingLinearDifference.lean 1 declarations
NestedBallCutoff.lean 7 declarations
NestedPositiveTestMeasure.lean 9 declarations
NoEulerCountersequence.lean 1 declarations
NoProjectedEulerSequence.lean 1 declarations
NullCompactCutoff.lean 2 declarations
OrthonormalHarmonicLipschitz.lean 2 declarations
OrthonormalImageSpan.lean 3 declarations
PhysicalBallMeasuredTests.lean 1 declarations
PhysicalProjectionEuler.lean 1 declarations
PointedBallTestError.lean 1 declarations
PointedEnergyCompactness.lean 1 declarations
PointedMetricBallTestError.lean 1 declarations
PointedTestLocalization.lean 2 declarations
PointedTestRecovery.lean 1 declarations
PointwiseIntegralBound.lean 1 declarations
PoissonActionFromScalar.lean 2 declarations
PoissonAffineTransfer.lean 1 declarations
PoissonAnnularEnergy.lean 2 declarations
PoissonBallEnergy.lean 1 declarations
PoissonBochnerMass.lean 1 declarations
PoissonCaccioppoli.lean 1 declarations
PoissonCommonRegion.lean 3 declarations
PoissonCompactExtension.lean 1 declarations
PoissonComparison.lean 2 declarations
PoissonCutoffEnergyBound.lean 1 declarations
PoissonCutoffErrors.lean 1 declarations
PoissonCutoffSource.lean 1 declarations
PoissonDefectBudget.lean 5 declarations
PoissonEnergyError.lean 3 declarations
PoissonEnergySubsolution.lean 1 declarations
PoissonFamilyGradient.lean 1 declarations
PoissonGradientBochner.lean 1 declarations
PoissonGradientBoundedness.lean 1 declarations
PoissonGradientBridge.lean 2 declarations
PoissonGradientConstruction.lean 1 declarations
PoissonGradientFromScalar.lean 1 declarations
PoissonGradientInput.lean 1 declarations
PoissonHarmonicCompactnessConstruction.lean 1 declarations
PoissonHarmonicCompactnessInput.lean 3 declarations
PoissonHarmonicLimitSubsequence.lean 1 declarations
PoissonHeight.lean 2 declarations
PoissonHessianFromScalar.lean 1 declarations
PoissonHessianIdentity.lean 3 declarations
PoissonHessianInput.lean 3 declarations
PoissonInteriorSmallRadii.lean 1 declarations
PoissonInteriorValues.lean 2 declarations
PoissonLocality.lean 3 declarations
PoissonMassUnits.lean 1 declarations
PoissonPairDefect.lean 1 declarations
PoissonPairSpan.lean 1 declarations
PoissonPathDefectBound.lean 1 declarations
PoissonPathDefectLimit.lean 1 declarations
PoissonProjectionGradient.lean 1 declarations
PoissonReplacement.lean 7 declarations
PoissonScalarFamily.lean 1 declarations
PoissonSecondOrderData.lean 1 declarations
PoissonShiftedMeasure.lean 1 declarations
PoissonSourceEstimates.lean 3 declarations
PoissonSourceLocalization.lean 2 declarations
PoissonSpan.lean 5 declarations
PoissonSpanLift.lean 4 declarations
PoissonSpanLinearLift.lean 3 declarations
PoissonStrongComparison.lean 2 declarations
PoissonUniformValue.lean 2 declarations
PoissonValueLimit.lean 1 declarations
PositiveCompactTestMeasure.lean 1 declarations
PositiveDefectCutoff.lean 2 declarations
PositiveDirichletFunctional.lean 3 declarations
PositiveDistancePoisson.lean 1 declarations
PositiveEnergyExcess.lean 2 declarations
PositiveSobolevTestMeasure.lean 1 declarations
PositiveSourceGradient.lean 8 declarations
PositiveSourceMoment.lean 5 declarations
PositiveSourceTail.lean 2 declarations
PositiveSourceTest.lean 10 declarations
PositiveSourceTruncation.lean 10 declarations
PositiveSublevelWindow.lean 2 declarations
PowerEnergyComparison.lean 1 declarations
PowerEnergyRates.lean 2 declarations
PowerSourceEnergyIdentity.lean 1 declarations
ProjectedEulerIdentity.lean 4 declarations
PublishedInputDischarge.lean 1 declarations
QuadraticBochnerCutoffLimit.lean 2 declarations
QuadraticCutoffIdentity.lean 3 declarations
QuadraticEnergyLimit.lean 1 declarations
QuadraticGradientComparison.lean 4 declarations
QuadraticLocalEnergy.lean 3 declarations
QuadraticValueGradientBound.lean 2 declarations
RCDPoissonEnergySubsolution.lean 1 declarations
RadialCutoffChange.lean 1 declarations
RadialCutoffEnergyIdentity.lean 2 declarations
RadialCutoffEnergyTransfer.lean 1 declarations
RadialCutoffIdentity.lean 9 declarations
RadialCutoffMass.lean 3 declarations
RadialCutoffNorm.lean 2 declarations
RadialCutoffStrongComparison.lean 1 declarations
RadialCutoffStrongLimit.lean 2 declarations
RadialEnergyUnits.lean 3 declarations
RadialEnergyVolume.lean 1 declarations
RadialInteriorEnergy.lean 1 declarations
RadialLocalSobolev.lean 4 declarations
RadialLocalSobolevLimit.lean 2 declarations
RadialPowerTest.lean 12 declarations
RadialSobolevMeasurableLimit.lean 1 declarations
RadialSobolevTimeMeasurable.lean 3 declarations
RadialSourceStrongGradient.lean 1 declarations
RawCutoffError.lean 1 declarations
RealCutoffConvergence.lean 1 declarations
ReciprocalWeightedTest.lean 1 declarations
RecoveredTestEnergy.lean 1 declarations
RecoveryEnergyFromSlope.lean 1 declarations
RemoveExceptionalTimes.lean 1 declarations
RescaledHarmonicEnergy.lean 1 declarations
RescaledLocalEnergyBound.lean 1 declarations
ResidualBochnerMass.lean 1 declarations
RightSlopeCorrection.lean 1 declarations
ScalarAbsorption.lean 4 declarations
ScalarBochnerConstruction.lean 1 declarations
ScalarDimensionalBochner.lean 3 declarations
ScaledCompactFactorGradient.lean 1 declarations
ScaledCompactFactorLipschitz.lean 1 declarations
ScaledCutoffIntegral.lean 1 declarations
ScaledCutoffL1.lean 2 declarations
ScaledCutoffPairings.lean 3 declarations
ScaledFixedCutoffNeighborhood.lean 3 declarations
ScaledGammaBound.lean 1 declarations
ScaledGammaError.lean 1 declarations
ScaledGammaExcess.lean 1 declarations
ScaledGradientGammaL2.lean 1 declarations
ScaledHamiltonJacobiGradient.lean 1 declarations
ScaledHessianYoungLimit.lean 1 declarations
ScaledRadialCutoffSobolev.lean 1 declarations
ScaledStampacchia.lean 3 declarations
ScaledUniformCutoff.lean 1 declarations
SharpLinearEnergyBound.lean 1 declarations
SharpNeighborhoodParameters.lean 1 declarations
SharpProjectionGradient.lean 1 declarations
SharpRecoveryEnergy.lean 1 declarations
SharpTestRecoverySequence.lean 1 declarations
SharpWeightedTestRecovery.lean 1 declarations
ShiftedBochnerCutoff.lean 3 declarations
ShiftedBochnerMeasure.lean 7 declarations
ShiftedDensityCutoffBound.lean 3 declarations
ShiftedDyadicSubsolutionLevels.lean 1 declarations
ShiftedRadonCutoff.lean 4 declarations
ShiftedSobolevProduct.lean 1 declarations
ShiftedSubsolutionLevelDecay.lean 1 declarations
ShortStepActionError.lean 1 declarations
SignedLipschitzMeasure.lean 3 declarations
SignedTestFunctional.lean 3 declarations
SmallBallPoissonQuadratic.lean 1 declarations
SmallBallPoissonValue.lean 2 declarations
SmallRadiusPoissonMean.lean 1 declarations
SmallScalePoissonGradient.lean 1 declarations
SmoothGradientTest.lean 2 declarations
SmoothLocalLipschitz.lean 1 declarations
SmoothRecoveryGradientBound.lean 1 declarations
SmoothTestDirectional.lean 1 declarations
SmoothTimeTestOrder.lean 1 declarations
SobolevAverageRepresentative.lean 1 declarations
SobolevCompactSupport.lean 2 declarations
SobolevGramPolarization.lean 1 declarations
SobolevHamiltonJacobiEndpoints.lean 1 declarations
SobolevLevelChain.lean 15 declarations
SobolevMultiplierProduct.lean 3 declarations
SobolevPointedTestRecovery.lean 1 declarations
SobolevPositivePower.lean 1 declarations
SobolevPowerGammaIntegrable.lean 1 declarations
SobolevPowerSourceIntegrable.lean 1 declarations
SobolevQuadraticEnergy.lean 3 declarations
SobolevSecondVariation.lean 1 declarations
SobolevSourceMassBound.lean 2 declarations
SobolevSumValueConvergence.lean 1 declarations
SobolevTestFunctional.lean 1 declarations
SobolevWeakEnergyLower.lean 4 declarations
SourceMassDifferenceEnergy.lean 1 declarations
SqrtDerivativeBound.lean 2 declarations
SquaredDistanceEnergy.lean 2 declarations
StampacchiaBound.lean 1 declarations
StampacchiaDecay.lean 2 declarations
SubsolutionCaccioppoli.lean 1 declarations
SubsolutionInterpolation.lean 3 declarations
SubsolutionL1Mean.lean 1 declarations
SubsolutionLevelDecay.lean 1 declarations
SubsolutionLevelMoment.lean 1 declarations
SubsolutionLevelStep.lean 1 declarations
SubsolutionSmallNorm.lean 1 declarations
SubsolutionSourceBound.lean 3 declarations
SubsolutionUnitMean.lean 1 declarations
SubsolutionUpperTailBound.lean 1 declarations
SubsolutionUpperTailGap.lean 1 declarations
SumEnergyConvergence.lean 1 declarations
SupportedEnergyLocality.lean 1 declarations
SupportedGammaIntegral.lean 1 declarations
SupportedGradientL2Error.lean 1 declarations
SupportedWeakSourceBound.lean 3 declarations
SupportedWeightedGamma.lean 1 declarations
SymmetricGammaForm.lean 4 declarations
TightL2Difference.lean 1 declarations
TimeEnergyIntervalBound.lean 1 declarations
TimeEnvelopeLipschitz.lean 1 declarations
TimeUniformMean.lean 2 declarations
TorsionBound.lean 1 declarations
TorsionMoment.lean 2 declarations
TorsionSuperlevel.lean 2 declarations
TranslatedMeanDerivative.lean 1 declarations
TransverseCutoffFlux.lean 1 declarations
TransverseTestError.lean 2 declarations
TransverseTestFormula.lean 1 declarations
UniformAnnularCoercivity.lean 1 declarations
UniformBallEnergyTest.lean 1 declarations
UniformCenteredConvergence.lean 1 declarations
UniformDensityEnergyTest.lean 1 declarations
UniformEnergyDensity.lean 1 declarations
UniformEnergyDerivative.lean 1 declarations
UniformEuclideanInnerTests.lean 1 declarations
UniformEventualLowerEnergy.lean 1 declarations
UniformGradientEnergy.lean 1 declarations
UniformLipschitzL2Limit.lean 2 declarations
UniformLocalizedLipschitzTests.lean 1 declarations
UniformLowerEnergyFromSequence.lean 1 declarations
UniformMetricMeasureTests.lean 2 declarations
UniformMovingValues.lean 1 declarations
UniformPhysicalInnerTests.lean 1 declarations
UniformRadialEnergy.lean 1 declarations
UniformRadialResolvent.lean 3 declarations
UniformRealAlgebra.lean 1 declarations
UniformSlicesSpacetimeL2GoodSet.lean 1 declarations
UniformSlicesWeightedIterated.lean 2 declarations
UniformSlicesWeightedLimit.lean 1 declarations
UniformVanishingGauge.lean 1 declarations
VanishingAnnuli.lean 2 declarations
VarianceLowerBound.lean 1 declarations
WeakBallMassBounds.lean 2 declarations
WeakBochnerSquare.lean 3 declarations
WeakCompactUniformTests.lean 2 declarations
WeakDensityDomination.lean 1 declarations
WeakEndpointWeights.lean 1 declarations
WeakEulerRigidity.lean 2 declarations
WeakFiniteDomination.lean 1 declarations
WeakHamiltonJacobiPairing.lean 2 declarations
WeakHarmonicRadialPairing.lean 2 declarations
WeakHarmonicWeightedPairing.lean 1 declarations
WeakInverseDensity.lean 1 declarations
WeakLaplacianAffineChain.lean 1 declarations
WeakLaplacianCutoff.lean 1 declarations
WeakLaplacianDomain.lean 3 declarations
WeakLaplacianFluxIdentity.lean 2 declarations
WeakLaplacianLowerMass.lean 1 declarations
WeakLaplacianMixedSourceL2.lean 3 declarations
WeakLaplacianOperator.lean 2 declarations
WeakLaplacianPowerProduct.lean 1 declarations
WeakLaplacianProduct.lean 1 declarations
WeakLaplacianSquare.lean 1 declarations
WeakLaplacianSupport.lean 2 declarations
WeakLaplacianWeightedProduct.lean 2 declarations
WeakLimitAnnuli.lean 1 declarations
WeakLocalizedTests.lean 1 declarations
WeakMapPerturbation.lean 1 declarations
WeakMapUniformIntegrals.lean 1 declarations
WeakMaximal.lean 4 declarations
WeakMinMass.lean 1 declarations
WeakPhysicalBallTests.lean 1 declarations
WeakRadialCancellation.lean 5 declarations
WeakSourceGradientBound.lean 1 declarations
WeakSubsolution.lean 3 declarations
WeightedBallEnergyLiminf.lean 1 declarations
WeightedEnergyDifference.lean 1 declarations
WeightedEnergyLiminf.lean 1 declarations
WeightedEnergyLower.lean 2 declarations
WeightedEnergyMap.lean 1 declarations
WeightedEnergyWeightLimit.lean 2 declarations
WeightedGammaGradientBound.lean 1 declarations
WeightedGammaJointLimit.lean 1 declarations
WeightedGammaL2Algebra.lean 4 declarations
WeightedGammaL2Continuity.lean 2 declarations
WeightedGammaLocality.lean 1 declarations
WeightedGammaYoung.lean 2 declarations
WeightedGradientDensity.lean 1 declarations
WeightedGradientPairDifference.lean 2 declarations
WeightedIntegralPotential.lean 3 declarations
WeightedL2SquareLimit.lean 1 declarations
WeightedLaplacianPair.lean 4 declarations
WeightedMatchedJoin.lean 19 declarations
WeightedMixedEnergy.lean 1 declarations
WeightedQuadraticEnergy.lean 2 declarations
WeightedRecoveryConvergence.lean 1 declarations
WeightedRecoveryEnergy.lean 1 declarations
WeightedSobolevIntegralLower.lean 1 declarations
WeightedTimeAverageEnergy.lean 1 declarations
WeightedWeakCauchyEnergy.lean 1 declarations
ZeroFractionCoercivity.lean 2 declarations