OAI/Analysis/BiholderTransport/Regularity/
480 declarations, 0 contain sorry, 0 declared as axioms; 161 files
Files
- AERademacher.lean 2 declarations
- ActionKernel.lean 4 declarations
- ActionLocalData.lean 1 declarations
- ActiveDifference.lean 4 declarations
- ActiveGraphLimit.lean 1 declarations
- ActiveLimit.lean 3 declarations
- ActiveOuter.lean 1 declarations
- ActualCenterRay.lean 2 declarations
- ActualLevels.lean 5 declarations
- ActualOutward.lean 1 declarations
- ActualParameter.lean 22 declarations
- ActualScaleSmallness.lean 4 declarations
- ActualSmallPlateau.lean 1 declarations
- ActualTransferInequality.lean 2 declarations
- Alignment.lean 4 declarations
- BundleSeparation.lean 1 declarations
- CenterDetCompact.lean 2 declarations
- CenterFullPullback.lean 2 declarations
- CenterPoleLimit.lean 3 declarations
- CenterPoleStationary.lean 1 declarations
- CenterRayLimit.lean 5 declarations
- CenterRegularCompact.lean 1 declarations
- CenterSequenceCompact.lean 2 declarations
- CenterSequenceOriginalLimit.lean 1 declarations
- CenterSequenceRegular.lean 1 declarations
- CenterTrueRayCompact.lean 1 declarations
- CenteredQuadratic.lean 3 declarations
- CompactAE.lean 9 declarations
- CompactDisk.lean 2 declarations
- CompactUniformSecondRemainder.lean 1 declarations
- ConfigurationCompact.lean 1 declarations
- ContDiffParametricQuadratic.lean 2 declarations
- ContDiffParametricSecant.lean 1 declarations
- ContDiffQuadraticUpper.lean 1 declarations
- ContDiffSecondOrder.lean 1 declarations
- ContDiffUncurryIterated.lean 2 declarations
- ContinuousClosedRelationSelector.lean 2 declarations
- CriticalChain.lean 1 declarations
- Diagonal.lean 1 declarations
- EuclideanUpper.lean 7 declarations
- FamilyComparison.lean 1 declarations
- FamilyGlobal.lean 2 declarations
- FiniteIntervalMesh.lean 2 declarations
- FiniteNonnegativeWeight.lean 1 declarations
- FiniteNonnegativeWeightPos.lean 2 declarations
- FiniteSimplexRepresentation.lean 1 declarations
- FirstActiveLimit.lean 1 import, no declarations
- FirstOutward.lean 1 declarations
- FixedJoinMiddle.lean 3 declarations
- FixedJoinUpper.lean 7 declarations
- FrameAbsorption.lean 1 declarations
- FrameDet.lean 4 declarations
- FrameMetric.lean 5 declarations
- FrameOutwardLimit.lean 1 declarations
- FunctionalDet.lean 1 declarations
- GeneratingKernel.lean 2 declarations
- GraphInverse.lean 3 declarations
- HopfApproximation.lean 6 declarations
- InteriorCompactUniqueFiber.lean 1 declarations
- InteriorMaximum.lean 7 declarations
- IntrinsicTestDet.lean 1 declarations
- InverseDifferenceGain.lean 3 declarations
- JointMovingPrefix.lean 5 declarations
- KernelBounds.lean 4 declarations
- LiftedSections.lean 5 declarations
- LimitGeometry.lean 6 declarations
- LipschitzSubAeDeriv.lean 4 declarations
- LocalMinSecondDeriv.lean 1 declarations
- LocalMinStrictGrowth.lean 1 declarations
- MaximumActiveCompact.lean 1 declarations
- MaximumActiveLimits.lean 2 declarations
- MaximumCenterCompact.lean 3 declarations
- MaximumCenterLimit.lean 2 declarations
- MaximumCenterLower.lean 1 declarations
- MaximumCenterRegular.lean 1 declarations
- MaximumCenterSequence.lean 4 declarations
- MaximumCenterSign.lean 2 declarations
- MaximumCenterUpper.lean 3 declarations
- MaximumCompact.lean 3 declarations
- MaximumConfiguration.lean 1 declarations
- MaximumDiagonal.lean 9 declarations
- MaximumEndpoint.lean 2 declarations
- MaximumFamily.lean 2 declarations
- MaximumGoodCenters.lean 1 declarations
- MaximumLowerBound.lean 1 declarations
- MaximumOuterBound.lean 1 declarations
- MaximumOuterSamples.lean 3 declarations
- MaximumOutward.lean 2 declarations
- MaximumOutwardCompact.lean 1 declarations
- MaximumPhaseCompact.lean 1 declarations
- MaximumPoleCompact.lean 2 declarations
- MaximumPoleSymmetric.lean 1 declarations
- MaximumReindex.lean 5 declarations
- MaximumRow.lean 3 declarations
- MaximumSample.lean 2 declarations
- MaximumSelectionCompact.lean 1 declarations
- MaximumSimultaneous.lean 1 declarations
- MaximumTemplateBound.lean 1 declarations
- MaximumTrueCenter.lean 1 declarations
- MaximumTrueOuter.lean 1 declarations
- MetricDefinitions.lean 23 declarations
- MinMax.lean 4 declarations
- MixedDetIntrinsic.lean 1 declarations
- MixedIntrinsic.lean 2 declarations
- ModifiedData.lean 5 declarations
- ModifiedOuterNeighborhood.lean 1 declarations
- ModifiedPhase.lean 2 declarations
- MovingCenterLower.lean 1 declarations
- MovingCenterUpper.lean 5 declarations
- MovingCrossing.lean 1 declarations
- MovingPrefix.lean 9 declarations
- NonnegativeTransfer.lean 1 declarations
- NormLower.lean 2 declarations
- NormMinMax.lean 5 declarations
- OriginalCenterLimit.lean 1 declarations
- OriginalOuterLimit.lean 1 declarations
- OuterBounds.lean 1 declarations
- OuterDetCompact.lean 1 declarations
- OuterIntrinsicDet.lean 1 declarations
- OuterIntrinsicSecond.lean 1 declarations
- OuterSplitLowerTest.lean 1 declarations
- OuterTemplate.lean 14 declarations
- OuterTemplatePrimitive.lean 9 declarations
- OuterVelocityFactorNonneg.lean 13 declarations
- OutwardClosed.lean 2 declarations
- OutwardWeightCap.lean 1 declarations
- ParametricActive.lean 4 declarations
- ParametricLowerSequence.lean 1 declarations
- PosSemidefApplyInner.lean 3 declarations
- PrefixAction.lean 6 declarations
- PullbackDet.lean 3 declarations
- RayAnchor.lean 7 declarations
- ReciprocalInverses.lean 1 declarations
- RestrictedTransform.lean 7 declarations
- Reversal.lean 2 declarations
- ReverseRegular.lean 5 declarations
- RiemannianMetricSegment.lean 1 declarations
- RoughLinear.lean 1 declarations
- SampleCenterFamilies.lean 2 declarations
- SecondFderivAdd.lean 1 declarations
- SecondFderivCompLinear.lean 1 declarations
- SecondScaled.lean 1 declarations
- ShortForward.lean 11 declarations
- ShortSelectorNonsingularity.lean 3 declarations
- SingularValuesBound.lean 1 declarations
- SmallAffineTimeTube.lean 1 declarations
- SmallEpsilon.lean 2 declarations
- SplitEndpointCost.lean 6 declarations
- SplitSelection.lean 3 declarations
- StationaryPullback.lean 9 declarations
- TemplateRightWeight.lean 4 declarations
- TrialBlowup.lean 2 declarations
- TrueCenterGain.lean 2 declarations
- TrueCenterLimit.lean 1 declarations
- UniformFiniteGrowth.lean 1 declarations
- UniformIntervalCrossing.lean 2 declarations
- UniformMiddle.lean 2 declarations
- UniformMixedBound.lean 6 declarations
- UniformShortMinima.lean 1 declarations
- UniformTestDet.lean 3 declarations
- UnitTime.lean 10 declarations