`OAI/Geometry/RCD/Heat/`

1183 declarations, 0 contain sorry, 0 declared as axioms; 609 files

Files

ACDerivativeL2Endpoint.lean 1 declarations
ActualHeatEnvelope.lean 4 declarations
ActualHeatGrams.lean 11 declarations
ActualHeatMass.lean 8 declarations
AlmostMonotoneAllTimes.lean 1 declarations
AlmostMonotoneTimeLimit.lean 1 declarations
AnnularHeatAverages.lean 1 declarations
AnnularHeatLipschitz.lean 1 declarations
AnnularKernelDifference.lean 2 declarations
AveragedHeatSource.lean 9 declarations
AveragedKernelDifference.lean 2 declarations
BakryLedouxHeatBochner.lean 1 declarations
BakryLedouxInput.lean 1 declarations
BakryLedouxScalarBochner.lean 2 declarations
BochnerHeatSmallness.lean 1 declarations
BoundedDensityGaussian.lean 1 declarations
BoundedExponentialIntegral.lean 3 declarations
BoundedHeatComplement.lean 1 declarations
BoundedHeatDiagonalHessianDifference.lean 1 declarations
BoundedHeatFullSource.lean 1 declarations
BoundedHeatGram.lean 2 declarations
BoundedHeatHessianL1Limit.lean 1 declarations
BoundedHeatIntegral.lean 2 declarations
BoundedHeatLimit.lean 2 declarations
BoundedHeatLogarithmicHessian.lean 1 declarations
BoundedHeatMixedGram.lean 2 declarations
BoundedHeatMixedGramBounds.lean 2 declarations
BoundedHeatMixedHessianDensity.lean 1 declarations
BoundedHeatMixedHessianVanishing.lean 1 declarations
BoundedHeatMixedMovingDensity.lean 1 declarations
BoundedHeatOrder.lean 8 declarations
BoundedHeatPowerMean.lean 3 declarations
BoundedHeatQuantitativeHessian.lean 1 declarations
BoundedHeatRepresentative.lean 6 declarations
BoundedHeatSecondVariation.lean 1 declarations
BoundedHeatSemigroup.lean 3 declarations
BoundedHeatSobolevData.lean 1 declarations
BoundedHeatVelocityHessian.lean 1 declarations
BoundedHeatVolumePower.lean 1 declarations
BoundedLocalLogarithm.lean 1 declarations
BoundedLpParts.lean 1 declarations
BoundedPlanHeatSecondVariation.lean 1 declarations
BoundedProductPowerIntegrable.lean 1 declarations
BoundedProductPowerRate.lean 1 declarations
BoundedSourceHeatBounds.lean 1 declarations
CanonicalAllTimeLogLimit.lean 1 declarations
CanonicalCompactEndpoints.lean 1 declarations
CanonicalCompactLogLimit.lean 1 declarations
CanonicalCompactLogLower.lean 1 declarations
CanonicalCompactLogUpper.lean 1 declarations
CanonicalDiagonalLower.lean 2 declarations
CanonicalFractionalKernelLog.lean 1 declarations
CanonicalGaussianDifference.lean 2 declarations
CanonicalGaussianUpper.lean 1 declarations
CanonicalHeatBackwardRatio.lean 1 declarations
CanonicalHeatHessian.lean 3 declarations
CanonicalHeatKernel.lean 8 declarations
CanonicalHeatTimeRatio.lean 1 declarations
CanonicalKernelConstruction.lean 5 declarations
CanonicalKernelIdentification.lean 3 declarations
CanonicalL2Rows.lean 8 declarations
CanonicalLocalBounds.lean 1 declarations
CanonicalLocalLower.lean 2 declarations
CanonicalMovingLogLower.lean 1 declarations
CanonicalNearDiagonal.lean 1 declarations
CanonicalPowerLower.lean 1 declarations
CanonicalRoughGaussianLower.lean 1 declarations
CanonicalRowLogLimit.lean 1 declarations
CanonicalStrictPositivity.lean 2 declarations
CanonicalUniformBridge.lean 1 declarations
CappedIntegralProduct.lean 4 declarations
CenteredActionLower.lean 1 declarations
CenteredActionRadiusBound.lean 1 declarations
CenteredHeatActionRealization.lean 1 declarations
CenteredHeatPlanEnergy.lean 1 declarations
CenteredWeightedPartition.lean 1 declarations
CompactEndpointKernelBounds.lean 2 declarations
CompactExponentialMultiplier.lean 3 declarations
CompactFactorLogGradient.lean 1 declarations
CompactFactorTimeRatio.lean 1 declarations
CompactHeatActionRealization.lean 1 declarations
CompactHeatActualPlanLimit.lean 1 declarations
CompactHeatBackwardSource.lean 1 declarations
CompactHeatBackwardSourceFormula.lean 1 declarations
CompactHeatBridge.lean 1 declarations
CompactHeatCommonHessianLimit.lean 2 declarations
CompactHeatContinuousLawLimit.lean 1 declarations
CompactHeatDensityGaussianTail.lean 1 declarations
CompactHeatDensityKernelBound.lean 1 declarations
CompactHeatDensityMoments.lean 2 declarations
CompactHeatDensityTailMoments.lean 1 declarations
CompactHeatDerivativeLipschitz.lean 1 declarations
CompactHeatDualLimit.lean 6 declarations
CompactHeatDualSaturation.lean 1 declarations
CompactHeatEnvelope.lean 1 declarations
CompactHeatFactors.lean 3 declarations
CompactHeatFirstDerivativeLimit.lean 1 declarations
CompactHeatGlobalHessianLimit.lean 1 declarations
CompactHeatGlobalIntrinsicHessian.lean 1 declarations
CompactHeatGlobalPower.lean 1 declarations
CompactHeatHalfDensityBound.lean 1 declarations
CompactHeatHarmonicAffineMean.lean 1 declarations
CompactHeatHarmonicSecondVariation.lean 1 declarations
CompactHeatHessian.lean 1 declarations
CompactHeatHessianL1Limit.lean 1 declarations
CompactHeatHessianTails.lean 1 declarations
CompactHeatHessianUniformBound.lean 1 declarations
CompactHeatInitialProduct.lean 1 declarations
CompactHeatInterpolation.lean 1 declarations
CompactHeatInterpolationLaws.lean 3 declarations
CompactHeatInterpolationMean.lean 2 declarations
CompactHeatIntrinsicHessian.lean 1 declarations
CompactHeatIntrinsicSecondDerivative.lean 1 declarations
CompactHeatIntrinsicSecondVariation.lean 1 declarations
CompactHeatJointConcentration.lean 2 declarations
CompactHeatJointGeodesic.lean 3 declarations
CompactHeatJointLaw.lean 8 declarations
CompactHeatJointLimit.lean 1 declarations
CompactHeatJointLogLimit.lean 3 declarations
CompactHeatJointSlack.lean 2 declarations
CompactHeatKernelScaling.lean 1 declarations
CompactHeatLaplaceLimit.lean 1 declarations
CompactHeatLaplacianRemainder.lean 3 declarations
CompactHeatLawLimits.lean 2 declarations
CompactHeatLimitMeanDerivative.lean 1 declarations
CompactHeatLimitOptimalTriplets.lean 1 declarations
CompactHeatLimitPlanIdentification.lean 1 declarations
CompactHeatLocalScaledHessianLimit.lean 3 declarations
CompactHeatLocalSourceMass.lean 1 declarations
CompactHeatLocalVelocityHessianLimit.lean 3 declarations
CompactHeatLocalizedSecondVariation.lean 1 declarations
CompactHeatLogarithmicContinuity.lean 1 declarations
CompactHeatMeanDifferentiable.lean 1 declarations
CompactHeatMeanLawLimit.lean 2 declarations
CompactHeatMeanTimeBound.lean 1 declarations
CompactHeatMeasure.lean 9 declarations
CompactHeatMixedOsmoticHessian.lean 1 declarations
CompactHeatOsmoticGradient.lean 1 declarations
CompactHeatOsmoticRate.lean 1 declarations
CompactHeatOsmoticTransfer.lean 1 declarations
CompactHeatOsmoticVanishing.lean 3 declarations
CompactHeatPowerDerivative.lean 2 declarations
CompactHeatPowerExtension.lean 1 declarations
CompactHeatPowerGronwall.lean 1 declarations
CompactHeatPowerMomentBound.lean 1 declarations
CompactHeatPowerRateBound.lean 1 declarations
CompactHeatPreservedLawLimit.lean 1 declarations
CompactHeatReferenceMass.lean 2 declarations
CompactHeatScaledHessian.lean 1 declarations
CompactHeatScaledHessianBound.lean 1 declarations
CompactHeatScalingCoupling.lean 7 declarations
CompactHeatScalingData.lean 2 declarations
CompactHeatScalingDensity.lean 4 declarations
CompactHeatSecondDerivativeBound.lean 1 declarations
CompactHeatSecondDerivativeLimit.lean 1 declarations
CompactHeatSecondVariationLimit.lean 1 declarations
CompactHeatStrongGradient.lean 1 declarations
CompactHeatTestTimeBound.lean 1 declarations
CompactHeatTimeReverse.lean 5 declarations
CompactHeatUniformDensity.lean 1 declarations
CompactHeatVelocityDecomposition.lean 2 declarations
CompactHeatVelocityHessianData.lean 1 declarations
CompactHeatVelocityHessianDecomposition.lean 2 declarations
CompactHeatVelocityHessianIdentity.lean 1 declarations
CompactHeatVelocityPotential.lean 2 declarations
CompactKernelFactor.lean 4 declarations
CompactLaplaceLimit.lean 1 declarations
CompactLipschitzHeatHessian.lean 1 declarations
CompactLogEquation.lean 1 declarations
CompactProductPowerDerivative.lean 1 declarations
CompactScaledLogBound.lean 1 declarations
CompactScalingActionLimits.lean 1 declarations
CompactScalingBoundary.lean 2 declarations
CompactSubsetTimePairing.lean 3 declarations
CompactTimePairing.lean 3 declarations
CompactTimePairingDerivative.lean 1 declarations
ConditionalPairInverse.lean 2 declarations
ContinuousKernelBridge.lean 1 declarations
ContinuousKernelContraction.lean 4 declarations
ContinuousKernelLog.lean 4 declarations
ContinuousKernelMarginalMass.lean 2 declarations
ContinuousKernelSaturation.lean 2 declarations
CutoffGaussianBlock.lean 1 declarations
DiagonalConditionalKernel.lean 2 declarations
DimensionalEVI.lean 1 declarations
DirectionalHeatError.lean 3 declarations
DiscreteGaussianComparison.lean 2 declarations
DominatedProductPowerDerivative.lean 1 declarations
DyadicHeatAt.lean 6 declarations
DyadicHeatAtStability.lean 1 declarations
DyadicHeatFamily.lean 7 declarations
DyadicHeatMeanComparison.lean 1 declarations
DyadicHeatStability.lean 1 declarations
DyadicMeanStability.lean 3 declarations
DyadicTimeIntegral.lean 2 declarations
EVIGeodesicConvexity.lean 1 declarations
EVIInitialLimit.lean 2 declarations
EntropyPowerBarrier.lean 6 declarations
EntropyPowerFirstVariation.lean 1 declarations
EntropyPowerRateContinuous.lean 6 declarations
EntropyPowerSemicontinuous.lean 1 declarations
EuclideanRadialKernel.lean 6 declarations
EuclideanRadialKernelDerivative.lean 2 declarations
EventualDyadicHeatCumulative.lean 1 declarations
EventualEnvelopeOrder.lean 1 declarations
EventualHeatCumulative.lean 1 declarations
ExactEntropyPower.lean 1 declarations
ExponentialHeatPower.lean 2 declarations
ExponentialIntegralBounds.lean 1 declarations
FiniteHeatMassShells.lean 3 declarations
FinitePrefixEnvelope.lean 4 declarations
FiniteScaleHeatError.lean 1 declarations
FirstOrderCompactHeatData.lean 1 declarations
FirstOrderHeatCoefficientPaths.lean 1 declarations
FirstOrderHeatEndpoint.lean 1 declarations
FirstOrderHeatMass.lean 1 declarations
FirstOrderHeatVelocityError.lean 1 declarations
FisherBochnerIdentity.lean 2 declarations
FisherEnergyCancellation.lean 2 declarations
FisherScalarComparison.lean 2 declarations
FisherSourceCancellation.lean 1 declarations
FisherSourceMoment.lean 3 declarations
FixedGaugeCalibration.lean 3 declarations
FixedGaugeTimeContinuous.lean 1 declarations
FixedGaugeTimePairing.lean 1 declarations
FixedHeatEnvelope.lean 2 declarations
GaussianActionSlack.lean 1 declarations
GaussianAnnularGradient.lean 1 declarations
GaussianBochnerShell.lean 1 declarations
GaussianBochnerTail.lean 1 declarations
GaussianBridgeKernelBound.lean 1 declarations
GaussianBridgeTail.lean 2 declarations
GaussianContinuousComparison.lean 2 declarations
GaussianCoshComparison.lean 3 declarations
GaussianCutoffError.lean 2 declarations
GaussianDensityTailMoments.lean 1 declarations
GaussianDyadicShells.lean 7 declarations
GaussianErrorBudget.lean 5 declarations
GaussianGradientAlgebra.lean 3 declarations
GaussianGridComparison.lean 1 declarations
GaussianHeatInput.lean 4 declarations
GaussianHyperbolicComparison.lean 1 declarations
GaussianIntegralEnvelope.lean 1 declarations
GaussianLinearGrowth.lean 3 declarations
GaussianLogUpper.lean 1 declarations
GaussianMassEnvelope.lean 4 declarations
GaussianMidpoint.lean 1 declarations
GaussianMomentEnvelope.lean 2 declarations
GaussianMomentIntegrable.lean 1 declarations
GaussianOffDiagonal.lean 5 declarations
GaussianScaleAbsorption.lean 3 declarations
GaussianShellKernel.lean 6 declarations
GaussianSubinterval.lean 1 declarations
GaussianTimeBlock.lean 2 declarations
GaussianTimeConvolution.lean 3 declarations
GaussianUpperAlgebra.lean 3 declarations
GaussianUpperEnvelope.lean 2 declarations
GaussianUpperHeatIncrement.lean 2 declarations
GaussianValueIntegrable.lean 1 declarations
GaussianVolumeMoment.lean 3 declarations
GaussianVolumeTail.lean 3 declarations
GlobalGaussianShell.lean 4 declarations
GlobalScaledLogSource.lean 1 declarations
HarmonicBochnerHeat.lean 5 declarations
HarmonicBochnerHeatSource.lean 3 declarations
HeatActionBasepoint.lean 7 declarations
HeatActionSlices.lean 1 declarations
HeatActionStrongGradient.lean 1 declarations
HeatAverageTwoTimeDual.lean 1 declarations
HeatBallPowerVolume.lean 1 declarations
HeatBaseBounds.lean 2 declarations
HeatBlockIntegrals.lean 3 declarations
HeatBlockVolumes.lean 2 declarations
HeatBochnerCutoffLimit.lean 1 declarations
HeatBochnerForm.lean 1 declarations
HeatBochnerIdentitySource.lean 1 declarations
HeatBoundedContinuousTest.lean 2 declarations
HeatBoundedLaplacian.lean 1 declarations
HeatBoundedMeasurableTest.lean 1 declarations
HeatBoundedSmoothing.lean 2 declarations
HeatBridgePairingDerivative.lean 2 declarations
HeatBridgeSecondDerivative.lean 5 declarations
HeatCanonicalHessianControl.lean 1 declarations
HeatCanonicalHessianVanishing.lean 1 declarations
HeatCappedOverlap.lean 6 declarations
HeatCompactUniform.lean 2 declarations
HeatCompactWeightedBochner.lean 1 declarations
HeatConcentration.lean 3 declarations
HeatControls.lean 1 declarations
HeatCumulative.lean 9 declarations
HeatCutoffEnergy.lean 3 declarations
HeatCutoffIntegral.lean 5 declarations
HeatCylinderEnergy.lean 2 declarations
HeatCylinderGluing.lean 1 declarations
HeatDaviesKernel.lean 3 declarations
HeatDensityConvolution.lean 5 declarations
HeatDensityL1Continuity.lean 4 declarations
HeatDensityL2.lean 2 declarations
HeatDensityTails.lean 1 declarations
HeatDetailedBalance.lean 4 declarations
HeatDirectionApproximation.lean 1 declarations
HeatEnergyDensity.lean 1 declarations
HeatEntropyInterpolation.lean 2 declarations
HeatEntropyVariation.lean 1 declarations
HeatEnvelopeContact.lean 2 declarations
HeatEnvelopeSegments.lean 1 declarations
HeatExhaustionScales.lean 6 declarations
HeatExpansionCoarse.lean 1 declarations
HeatExponentialEnergy.lean 2 declarations
HeatExponentialVariation.lean 4 declarations
HeatExteriorDecay.lean 3 declarations
HeatFisherCurvature.lean 1 declarations
HeatFisherDimensional.lean 2 declarations
HeatFisherRiccati.lean 1 declarations
HeatFisherVariation.lean 1 declarations
HeatFullMassBound.lean 1 declarations
HeatGamma.lean 1 declarations
HeatGammaEnergyEstimate.lean 1 declarations
HeatGammaSobolev.lean 1 declarations
HeatGaussianRadius.lean 5 declarations
HeatGeneralRepresentation.lean 3 declarations
HeatGeneratorAmplitude.lean 2 declarations
HeatGeneratorSecondDerivative.lean 3 declarations
HeatGeneratorTimeContinuity.lean 3 declarations
HeatGramComparison.lean 2 declarations
HeatGramError.lean 5 declarations
HeatGramEvolution.lean 6 declarations
HeatGramRebase.lean 3 declarations
HeatHalfVolume.lean 1 declarations
HeatHamiltonPositive.lean 1 declarations
HeatHamiltonWeighted.lean 1 declarations
HeatHarmonicMassControl.lean 1 declarations
HeatInwardDecay.lean 1 declarations
HeatIteratedLaplacian.lean 3 declarations
HeatJointDensity.lean 7 declarations
HeatJointSymmetry.lean 3 declarations
HeatKernelDifferenceInput.lean 1 declarations
HeatKernelRows.lean 15 declarations
HeatKernelSemigroup.lean 2 declarations
HeatLaplacianContraction.lean 2 declarations
HeatLevelEnergy.lean 2 declarations
HeatLevelIntegral.lean 4 declarations
HeatLevelMass.lean 4 declarations
HeatLiYau.lean 2 declarations
HeatLiYauParameter.lean 1 declarations
HeatLiYauParameterWeighted.lean 1 declarations
HeatLiYauWeighted.lean 1 declarations
HeatLocalBochnerMass.lean 1 declarations
HeatLocalEnergy.lean 4 declarations
HeatLocalOsmoticEstimate.lean 1 declarations
HeatLocalSmoothing.lean 2 declarations
HeatLocalSourceConvergence.lean 1 declarations
HeatLocalizedLiYau.lean 1 declarations
HeatLogarithmData.lean 2 declarations
HeatLogarithmicSlopeBound.lean 1 declarations
HeatMarkovKernel.lean 5 declarations
HeatMassDiagonalSelection.lean 1 declarations
HeatMassIncrement.lean 2 declarations
HeatMassSmoothing.lean 2 declarations
HeatMassTail.lean 2 declarations
HeatMassTimeContinuity.lean 3 declarations
HeatMeanComparison.lean 1 declarations
HeatMeanStrongLimit.lean 1 declarations
HeatMeasureAbsoluteContinuity.lean 2 declarations
HeatMeasureConservation.lean 3 declarations
HeatMeasureEvolution.lean 3 declarations
HeatMeasureMass.lean 3 declarations
HeatMeasureMassContinuity.lean 3 declarations
HeatMeasureProbability.lean 3 declarations
HeatMixedGramEnergy.lean 1 declarations
HeatNonlinearPairingDerivative.lean 1 declarations
HeatOffDiagonalL2.lean 4 declarations
HeatOsmoticNoiseRate.lean 1 declarations
HeatOverlapDiagonalLower.lean 3 declarations
HeatOverlapFinite.lean 4 declarations
HeatOverlapKernel.lean 5 declarations
HeatPairMeasure.lean 7 declarations
HeatParabolicDecay.lean 1 declarations
HeatParabolicSmall.lean 1 declarations
HeatParabolicStep.lean 1 declarations
HeatPlanFirstVariation.lean 1 declarations
HeatPlanQuadraticEnergy.lean 1 declarations
HeatPlanWeakVelocity.lean 2 declarations
HeatPointEvaluation.lean 3 declarations
HeatPointwiseDecay.lean 1 declarations
HeatPointwiseDisplacement.lean 1 declarations
HeatPointwiseTwoTimeDual.lean 1 declarations
HeatPoissonAverage.lean 4 declarations
HeatPoleIncrements.lean 2 declarations
HeatPowerEnergyBalance.lean 1 declarations
HeatPowerIntegrability.lean 2 declarations
HeatPowerTailDomination.lean 1 declarations
HeatProductSourceCancellation.lean 1 declarations
HeatRadonDensity.lean 7 declarations
HeatReferenceEVI.lean 1 declarations
HeatRegimeBridges.lean 3 declarations
HeatRelativeTangent.lean 5 declarations
HeatReverseEntropy.lean 1 declarations
HeatReversePoincare.lean 2 declarations
HeatScalarLaplacianPairing.lean 2 declarations
HeatSecondSourcePairing.lean 1 declarations
HeatShiftedHessianBound.lean 1 declarations
HeatSmoothingScale.lean 2 declarations
HeatSobolevWeightedBochner.lean 1 declarations
HeatSquarePairing.lean 1 declarations
HeatTailGradient.lean 1 declarations
HeatTimeContinuity.lean 4 declarations
HeatToleranceSelection.lean 1 declarations
HeatTransitionDecay.lean 3 declarations
HeatTransitionPointwise.lean 2 declarations
HeatUniformTails.lean 2 declarations
HeatUpperIncrement.lean 1 declarations
HeatVarianceBounded.lean 1 declarations
HeatVarianceContinuity.lean 3 declarations
HeatVarianceDerivative.lean 2 declarations
HeatVarianceForms.lean 2 declarations
HeatVarianceLower.lean 1 declarations
HeatVarianceSobolev.lean 1 declarations
HeatWeightedEvaluation.lean 3 declarations
HeatWeightedRows.lean 1 declarations
HessianForwardOsmotic.lean 3 declarations
HessianLogarithmicDirections.lean 1 declarations
KernelDensityContinuity.lean 2 declarations
KernelDensityTime.lean 4 declarations
KernelDifferenceTransform.lean 2 declarations
KernelGaussianDifference.lean 2 declarations
KernelGradientFromReverse.lean 1 declarations
KernelHalfBound.lean 1 declarations
KernelHeatBackwardContinuity.lean 2 declarations
KernelHeatCompactPowerDerivative.lean 1 declarations
KernelHeatComplementMonotone.lean 1 declarations
KernelHeatContinuityEquation.lean 1 declarations
KernelHeatGeneratorBochner.lean 2 declarations
KernelHeatGeneratorDerivative.lean 4 declarations
KernelHeatGlobalPowerDerivative.lean 1 declarations
KernelHeatInitialLimit.lean 1 declarations
KernelHeatInitialUniqueness.lean 1 declarations
KernelHeatL2Representation.lean 2 declarations
KernelHeatLipschitzDisplacement.lean 2 declarations
KernelHeatLogarithmicContinuity.lean 1 declarations
KernelHeatLogarithmicEquation.lean 1 declarations
KernelHeatLogarithmicLiYau.lean 1 declarations
KernelHeatOrder.lean 3 declarations
KernelHeatProductDerivative.lean 2 declarations
KernelHeatScaledBochner.lean 1 declarations
KernelHeatSharpLipschitz.lean 1 declarations
KernelHeatSourceLower.lean 1 declarations
KernelHeatSourceUpper.lean 2 declarations
KernelHeatSpatialSource.lean 1 declarations
KernelHeatTemporalBound.lean 2 declarations
KernelHeatTimeContinuity.lean 1 declarations
KernelHeatTimeDerivative.lean 2 declarations
KernelHeatTimeDifference.lean 1 declarations
KernelHeatTimeMonotone.lean 1 declarations
KernelHeatWindowBounds.lean 1 declarations
KernelLogConstants.lean 1 declarations
KernelLogMarginals.lean 1 declarations
KernelMeasureBounds.lean 10 declarations
KernelRowL2.lean 4 declarations
KernelScalingFixedPoint.lean 2 declarations
KernelTwoTimeAbsoluteSlope.lean 1 declarations
KernelTwoTimeSlope.lean 1 declarations
LiYauFisherBound.lean 1 declarations
LiYauParameterAlgebra.lean 1 declarations
LiYauParameterBound.lean 1 declarations
LiYauRiccatiAlgebra.lean 1 declarations
LipschitzTimePairing.lean 3 declarations
LocalHeatRepresentative.lean 1 declarations
LocalLogarithmGammaByValue.lean 1 declarations
LocalLogarithmicDifferenceFlux.lean 1 declarations
LocalLogarithmicFluxBound.lean 1 declarations
LocalLogarithmicGradient.lean 2 declarations
LocalLogarithmicLaplacian.lean 1 declarations
LocalLogarithmicSumFlux.lean 1 declarations
LocalScaledLogSource.lean 1 declarations
LocalSmoothLogarithm.lean 1 declarations
LocalSmoothLogarithmC3.lean 1 declarations
LocalizedLiYauIntegral.lean 3 declarations
LocalizedOsmoticNoiseRate.lean 1 declarations
LogarithmicEnergyIdentity.lean 3 declarations
LogarithmicSquareGram.lean 1 declarations
LongAverageGaussian.lean 1 declarations
LongAverageHeatBound.lean 3 declarations
MissingHeatMass.lean 2 declarations
NearEndpointTransfer.lean 1 declarations
NearbyHeatEndpoint.lean 1 declarations
NonnegativeKernelBridgeMass.lean 1 declarations
NonpositiveBakryLedoux.lean 1 declarations
OptimalHeatCalibration.lean 1 declarations
OptimalHeatPlanCalibration.lean 1 declarations
OsmoticEnergyAlgebra.lean 1 declarations
OsmoticNoiseRate.lean 1 declarations
PairedHeatActionLimits.lean 1 declarations
ParabolicDyadicAlgebra.lean 4 declarations
PoissonHeatShiftedMass.lean 1 declarations
PositiveKernelLogDerivative.lean 4 declarations
PositiveKernelOscillation.lean 1 declarations
PositiveKernelScaling.lean 2 declarations
PowerLogSourceIntegral.lean 2 declarations
PowerRateBound.lean 1 declarations
PrescribedHeatEndpoint.lean 1 declarations
QuadraticHeatBochnerMass.lean 2 declarations
RebasedHeatMeanComparison.lean 1 declarations
RelativeHeatMean.lean 1 declarations
RenyiFisherBounds.lean 2 declarations
RescaledHeatEnvelope.lean 3 declarations
RiccatiFiniteInterval.lean 1 declarations
RiccatiInitialBound.lean 1 declarations
ScaledCompactFactorTimeLower.lean 2 declarations
ScaledCompactReferenceBounds.lean 1 declarations
ScaledCompactSpacetimeBound.lean 1 declarations
ScaledDyadicHeatComparison.lean 1 declarations
ScaledGaussianTail.lean 3 declarations
ScaledHamiltonBound.lean 1 declarations
ScaledHamiltonNoiseBound.lean 1 declarations
ScaledHeatActionLimit.lean 4 declarations
ScaledHeatAffinePlan.lean 1 declarations
ScaledHeatAllTimes.lean 1 declarations
ScaledHeatAtBounds.lean 1 declarations
ScaledHeatAveragedGradient.lean 1 declarations
ScaledHeatAveragedHamiltonJacobi.lean 1 declarations
ScaledHeatAveragedPlan.lean 1 declarations
ScaledHeatBase.lean 2 declarations
ScaledHeatBridgeSecondDerivative.lean 1 declarations
ScaledHeatContinuousCylinder.lean 1 declarations
ScaledHeatContinuousHamiltonJacobi.lean 1 declarations
ScaledHeatContinuousLimit.lean 1 declarations
ScaledHeatControls.lean 1 declarations
ScaledHeatCountableRegions.lean 1 declarations
ScaledHeatCutoffEnergy.lean 1 declarations
ScaledHeatCutoffEnergyLimit.lean 1 declarations
ScaledHeatGlobalCompactness.lean 1 declarations
ScaledHeatGradientTimeDerivative.lean 1 declarations
ScaledHeatGramBound.lean 2 declarations
ScaledHeatHamiltonJacobiFromCompactness.lean 1 declarations
ScaledHeatHessianLimit.lean 1 declarations
ScaledHeatIntervalEnergy.lean 1 declarations
ScaledHeatIteratedFromCompactness.lean 1 declarations
ScaledHeatJointEquation.lean 1 declarations
ScaledHeatLimitPointwiseTime.lean 1 declarations
ScaledHeatLimitTimeBound.lean 1 declarations
ScaledHeatLipschitzEnergy.lean 1 declarations
ScaledHeatLogTimeData.lean 4 declarations
ScaledHeatMassShells.lean 1 declarations
ScaledHeatMeasurableSobolev.lean 1 declarations
ScaledHeatPlanComparison.lean 1 declarations
ScaledHeatPlanVariation.lean 1 declarations
ScaledHeatPointwiseComparison.lean 1 declarations
ScaledHeatTimeAverageEnergy.lean 1 declarations
ScaledHeatTimeBound.lean 1 declarations
ScaledHeatTimePairing.lean 1 declarations
ScaledHeatTransportLimit.lean 1 declarations
ScaledHeatValueError.lean 1 declarations
ScaledHeatWeakEnergy.lean 1 declarations
ScaledKernelCoupling.lean 4 declarations
ScaledLiYauRemainder.lean 1 declarations
ScaledLiYauSource.lean 1 declarations
ScaledLogBridge.lean 1 declarations
ScaledLogPairBounds.lean 2 declarations
ScaledLogarithmSelfGamma.lean 1 declarations
ScaledNoiseGradient.lean 1 declarations
ScaledNoiseLipschitz.lean 1 declarations
ScaledRebasedHeatComparison.lean 1 declarations
ScaledReferenceError.lean 2 declarations
ScaledTimeError.lean 1 declarations
ScalingBoundaryLimit.lean 1 declarations
ScalingKernelProductBound.lean 1 declarations
ScalingLogPartition.lean 1 declarations
SelectedHarmonicHeatMass.lean 1 declarations
SeparatedGaussianBound.lean 1 declarations
SeparatedSourceBounds.lean 2 declarations
ShiftedLogarithmPairing.lean 2 declarations
ShiftedLogarithmSquare.lean 2 declarations
ShortAverageGaussian.lean 2 declarations
ShortAverageHeatBound.lean 1 declarations
SlowHeatGrowth.lean 5 declarations
SmallNoiseActionLipschitz.lean 1 declarations
SmallNoiseLogBounds.lean 1 declarations
SmallNoiseLogScale.lean 1 declarations
SmallRadiusHeatSecondVariation.lean 1 declarations
SmallRadiusOriginalMean.lean 1 declarations
SourceComparisonIdentity.lean 1 declarations
SourceTimeIntegrability.lean 2 declarations
SpaceTimeIncrement.lean 1 declarations
SpaceTimeSlopeRate.lean 3 declarations
SummableShellTail.lean 2 declarations
SupportedGaussianVolume.lean 1 declarations
SupportedHeatEnvelope.lean 3 declarations
TimeLowerEnvelope.lean 8 declarations
TwoRateEvolution.lean 1 declarations
TwoTimeCostLimit.lean 2 declarations
UniformCenteredSecondVariation.lean 1 declarations
UniformCumulativeConstants.lean 1 declarations
UniformDyadicHeatBounds.lean 1 declarations
UniformHeatActionCenter.lean 1 declarations
UniformHeatActionLower.lean 1 declarations
UniformHeatActionRealization.lean 1 declarations
UniformHeatAtBounds.lean 1 declarations
UniformHeatBase.lean 2 declarations
UniformHeatComparisonParameters.lean 2 declarations
UniformHeatControlsAt.lean 1 declarations
UniformHeatCumulative.lean 1 declarations
UniformHeatMassIncrement.lean 2 declarations
UniformHeatMassTail.lean 4 declarations
UniformHeatMeanComparison.lean 1 declarations
UniformSupportedHeatBounds.lean 1 declarations
UnitIntervalGaussianComparison.lean 1 declarations
WeightedLaplaceLimit.lean 1 declarations
WeightedSourceSquare.lean 1 declarations