OAI/Geometry/Perimeter/Regularity/
1579 declarations, 0 contain sorry, 0 declared as axioms; 176 files
Files
- ActualFiberFirstMoment.lean 5 declarations
- ActualFiberMoments.lean 3 declarations
- ActualFiberSecondMoment.lean 1 declarations
- ActualFiberZerothMoment.lean 3 declarations
- ActualFluxWindowLimit.lean 3 declarations
- AnnularCutoffTestAdmissible.lean 29 declarations
- BlowupHolderGraph.lean 1 declarations
- BlowupHomeomorph.lean 16 declarations
- C1Graph.lean 1 declarations
- C1MinRegularTest.lean 8 declarations
- ClosedFilledLineInvariantOfFrontier.lean 2 declarations
- CompactLpExtension.lean 7 declarations
- ConeLinkIntersection.lean 5 declarations
- ConeLinkSupport.lean 7 declarations
- ConeRadialCap.lean 15 declarations
- ContinuousWithinAtSurfaceGradientOfLocalLevel.lean 28 declarations
- CoupledConeLink.lean 10 declarations
- DilatedVolumeTest.lean 16 declarations
- EllipticC1Limit.lean 2 declarations
- EllipticC1Parts.lean 4 declarations
- EllipticC1Test.lean 6 declarations
- EllipticCaccioppoli.lean 5 declarations
- EllipticCaccioppoliAlgebra.lean 5 declarations
- EllipticCompactGradient.lean 2 declarations
- EllipticContinuousComparison.lean 5 declarations
- EllipticContraction.lean 3 declarations
- EllipticCurl.lean 16 declarations
- EllipticCutField.lean 6 declarations
- EllipticCutoffEnergy.lean 2 declarations
- EllipticDifference.lean 11 declarations
- EllipticExcessStep.lean 1 declarations
- EllipticFamilyEstimate.lean 3 declarations
- EllipticGradientLimit.lean 3 declarations
- EllipticHarmonicBounds.lean 2 declarations
- EllipticHilbert.lean 3 declarations
- EllipticHodge.lean 5 declarations
- EllipticHodgeIdentity.lean 4 declarations
- EllipticIteration.lean 2 declarations
- EllipticLinearStep.lean 6 declarations
- EllipticLocalExtension.lean 4 declarations
- EllipticLocalNorm.lean 10 declarations
- EllipticLocality.lean 7 declarations
- EllipticOneScale.lean 6 declarations
- EllipticPointwise.lean 1 declarations
- EllipticRescale.lean 9 declarations
- EllipticScaleStep.lean 4 declarations
- EllipticSecant.lean 5 declarations
- EllipticSecantBounds.lean 4 declarations
- EllipticSlopeComparison.lean 4 declarations
- EllipticTestSpace.lean 14 declarations
- EllipticUniformGradient.lean 2 declarations
- ExistsCompactTraceOnBounded.lean 32 declarations
- ExistsDiameterCoverOfHausdorffZero.lean 13 declarations
- ExistsLocalPolarEqApproximateNormal.lean 24 declarations
- ExistsLocalVariationExtension.lean 10 declarations
- ExistsMinimizingBoundaryAreaGrowth.lean 18 declarations
- ExistsMinimizingDensityLimit.lean 16 declarations
- ExistsTangentialGradientBallBound.lean 12 declarations
- FiberAveraging.lean 6 declarations
- FiberCompactness.lean 13 declarations
- FiberCrossing.lean 9 declarations
- FiberHeight.lean 23 declarations
- FiberLocalization.lean 4 declarations
- FiberMomentIntegration.lean 5 declarations
- FiberQuadraticLimit.lean 5 declarations
- FlatExcess.lean 23 declarations
- FlatnessImprovement.lean 3 declarations
- GeoAlgebra.lean 9 declarations
- GeoComposition.lean 5 declarations
- GeoRegularity.lean 10 declarations
- GeometricDerivativeModulus.lean 1 declarations
- GeometricHausdorff.lean 41 declarations
- GeometricHolder.lean 7 declarations
- GeometricHolderAlgebra.lean 4 declarations
- GradientContDiff.lean 17 declarations
- GraphChart.lean 13 declarations
- GraphCoordinates.lean 3 declarations
- GraphDerivative.lean 5 declarations
- GraphExistence.lean 4 declarations
- GraphFluxWeight.lean 5 declarations
- GraphGeoCoordinates.lean 1 declarations
- GraphNormal.lean 9 declarations
- GraphPhase.lean 1 declarations
- GraphSlope.lean 1 declarations
- GraphTestLift.lean 6 declarations
- HalfspaceHorizontal.lean 2 declarations
- HarmonicApproxIdentity.lean 2 declarations
- HarmonicHeightLimit.lean 3 declarations
- HarmonicKernel.lean 19 declarations
- HarmonicLimitBounds.lean 4 declarations
- HarmonicTaylor.lean 9 declarations
- HasC1TraceAt.lean 21 declarations
- HeightCompactness.lean 7 declarations
- HeightMeanValue.lean 15 declarations
- HolderGraph.lean 1 declarations
- IndicatorConvolutionVariationLocalLe.lean 9 declarations
- InitialSlab.lean 2 declarations
- IntegralDivergenceEqZero.lean 16 declarations
- IntegralDivergenceEqZeroOfPerimeterEqZero.lean 9 declarations
- IntegralInnerEqInnerToLp.lean 13 declarations
- IsConeMemPosTangentCone.lean 3 declarations
- IsometricMinimizer.lean 7 declarations
- LinearBaseGain.lean 3 declarations
- LinearDerivativeGain.lean 2 declarations
- LinearDifference.lean 3 declarations
- LinearLocalGain.lean 2 declarations
- LinearSchauder.lean 2 declarations
- LinearWeakDerivative.lean 2 declarations
- LocalFlatExcess.lean 3 declarations
- Main.lean 7 imports, no declarations
- MinimalFlux.lean 5 declarations
- MinimalGraphEquation.lean 1 declarations
- MinimalGraphSmooth.lean 1 declarations
- MollifiedFiberMoment.lean 8 declarations
- NeighborhoodPlanes.lean 3 declarations
- NonlinearDerivativeGain.lean 5 declarations
- NonlinearLocalGain.lean 3 declarations
- NonlinearSmooth.lean 2 declarations
- NormalAdjustment.lean 5 declarations
- NormalCoordinates.lean 10 declarations
- NormalFluxError.lean 1 declarations
- NormalPhaseMollification.lean 8 declarations
- NormalWindowTest.lean 14 declarations
- NormalizedHeight.lean 10 declarations
- PairedCutTest.lean 24 declarations
- PerimeterAdmissiblePartitionPiece.lean 23 declarations
- PerimeterEqOfAe.lean 36 declarations
- PerimeterMomentLimit.lean 4 declarations
- PhaseMomentLimit.lean 9 declarations
- PhaseRestoration.lean 2 declarations
- PhaseSupportBlownUpSet.lean 2 declarations
- PlaneFiberCompactness.lean 10 declarations
- PlaneHeightLimit.lean 5 declarations
- PlaneHeightResidual.lean 5 declarations
- PlaneLaplacian.lean 8 declarations
- PlaneWindowLift.lean 9 declarations
- QuadraticError.lean 1 declarations
- QuadraticMoment.lean 9 declarations
- RankOneNormalError.lean 23 declarations
- RawConeLink.lean 73 declarations
- RegularSupersolutionC1Test.lean 10 declarations
- SequentialFlatness.lean 3 declarations
- SetIntegralSubLeSymmDiff.lean 15 declarations
- SingleGraph.lean 2 declarations
- SlabContraction.lean 1 declarations
- SlabIteration.lean 5 declarations
- SlabScaling.lean 3 declarations
- SmoothFlatOrder.lean 16 declarations
- SmoothLayerSumBounds.lean 13 declarations
- SmoothSheet.lean 5 declarations
- SmoothSublevelPairingBound.lean 24 declarations
- SmulMemPhaseSupport.lean 26 declarations
- Space.lean 29 declarations
- SphericalFrankel.lean 37 declarations
- SupportAffineEstimate.lean 5 declarations
- SupportImprovement.lean 2 declarations
- SurfaceGradientComp.lean 21 declarations
- SurfaceGradientConstSub.lean 11 declarations
- TangentPlanes.lean 3 declarations
- TangentialGradientComp.lean 33 declarations
- TendstoLintegralNormOfL2.lean 10 declarations
- TendstoWeightedHalfspaceBlowup.lean 20 declarations
- TotallyBoundedRangeOfUniformApproximation.lean 17 declarations
- TsupportBlowdownSubsetBall.lean 17 declarations
- UniformDerivativeContinuity.lean 2 declarations
- UniformFlatness.lean 2 declarations
- VectorEnergy.lean 22 declarations
- VectorQuotient.lean 6 declarations
- WeakDerivative.lean 4 declarations
- WeakHarmonicRadial.lean 8 declarations
- WeakHarmonicSmooth.lean 7 declarations
- WeightedFiberMoment.lean 3 declarations
- WeightedSquareLimit.lean 1 declarations
- WeightedWrongWayFlux.lean 2 declarations
- WholeBoundarySublevelMeasureStep.lean 18 declarations
- WindowAverage.lean 14 declarations