OAI/Analysis/RieszRectifiability/Foundations/
313 declarations, 0 contain sorry, 0 declared as axioms; 98 files
Files
- ADGramSlices.lean 2 declarations
- ADHoleDensity.lean 4 declarations
- AdmissibleDyadicHorizon.lean 3 declarations
- AnnularAverageComparison.lean 1 declarations
- AnnularBoundedTangents.lean 5 declarations
- AnnularDescendantTotalMass.lean 2 declarations
- AnnularDimensionTermination.lean 2 declarations
- BallLipschitzExtension.lean 2 declarations
- BlowupBilateralCenters.lean 2 declarations
- BlowupExcess.lean 3 declarations
- BlowupMeasure.lean 7 declarations
- BlowupOscillation.lean 3 declarations
- BoundedDensityWeights.lean 4 declarations
- BoundedDisplacementConvexContraction.lean 1 declarations
- BoundedDisplacementProperMap.lean 2 declarations
- BoundedPlanarDensity.lean 4 declarations
- BoundedSupportEnergy.lean 2 declarations
- CapErrorRows.lean 2 declarations
- CappedDensityEquation.lean 1 declarations
- CappedLowerGrowth.lean 5 declarations
- CappedLowerSupportTubes.lean 2 declarations
- CappedLowerTangents.lean 3 declarations
- CappedTestSymmetry.lean 6 declarations
- CappedTransform.lean 5 declarations
- CappedTransformAdjoint.lean 2 declarations
- CappedTransformL2.lean 1 declarations
- ClosedBallMeasureComparison.lean 1 declarations
- CoherentRegionParameterization.lean 4 declarations
- CoordinatePieceParameterization.lean 2 declarations
- DensityGradientEquation.lean 1 declarations
- DyadicApproximateFits.lean 1 declarations
- DyadicChainPropagation.lean 1 declarations
- DyadicDistanceSteps.lean 1 declarations
- DyadicDistanceSum.lean 3 declarations
- DyadicExcessSchedule.lean 3 declarations
- DyadicFitCalibration.lean 3 declarations
- DyadicLipschitzFamily.lean 7 declarations
- DyadicPropagationRadii.lean 7 declarations
- EmptyBallHalfspace.lean 4 declarations
- ExcessPropagationSchedule.lean 9 declarations
- FineCoherentRegions.lean 7 declarations
- FiniteChargeSelection.lean 2 declarations
- FiniteMassSurvival.lean 2 declarations
- FiniteNormalizedWeights.lean 10 declarations
- FinitePieceCoordinates.lean 4 declarations
- FiniteSupportRefinements.lean 5 declarations
- FullSupportFromAnnuli.lean 1 declarations
- GeometricGramRows.lean 3 declarations
- GlobalLowerDiameter.lean 1 declarations
- GrowthHausdorffDomination.lean 2 declarations
- GrowthVolumeDomination.lean 3 declarations
- HardExteriorOscillation.lean 3 declarations
- HoleTangentMeasure.lean 2 declarations
- ImmediateChildPartition.lean 7 declarations
- IndexedSeedChainCounting.lean 1 declarations
- IsometricLocalTransforms.lean 5 declarations
- JointFitBasePoints.lean 1 declarations
- JointSupportAnchors.lean 1 declarations
- LargeSubsetEscape.lean 2 declarations
- LocalImageCapture.lean 2 declarations
- LocalInteriorRepresentative.lean 1 declarations
- LocalTestConstancy.lean 2 declarations
- MeasureBounds.lean 8 declarations
- NativeHausdorffGrowth.lean 2 declarations
- NeighboringFitErrors.lean 4 declarations
- NoncollapsingRegionRepresentatives.lean 2 declarations
- NormalizedGramDecay.lean 4 declarations
- NormalizedLocalEnergyBasic.lean 3 declarations
- NormalizedSetIndicators.lean 9 declarations
- OriginalDyadicTests.lean 7 declarations
- OriginalOscillationWitness.lean 3 declarations
- PlanarPullbackMeasure.lean 8 declarations
- PositiveNormalPotential.lean 10 declarations
- QuadraticNormalPotential.lean 4 declarations
- RegionRepresentativeGeometry.lean 4 declarations
- SeedChainCounting.lean 2 declarations
- SeedMultiplicityIntegration.lean 4 declarations
- SeparatedParameterPatchGluing.lean 3 declarations
- SeparatedSmoothAnnuli.lean 2 declarations
- ShrinkingBallIntegrals.lean 2 declarations
- SmoothAnnularGapWitness.lean 1 declarations
- SmoothAnnularIntegrability.lean 2 declarations
- SmoothAnnularNormalPotential.lean 3 declarations
- SmoothAnnularRescaling.lean 5 declarations
- SmoothAnnularTangentBounds.lean 1 declarations
- SmoothAnnularWeights.lean 8 declarations
- SourceDensityConstant.lean 2 declarations
- SourceNormalizedEnergy.lean 1 declarations
- SourceNormalizedRegionData.lean 1 declarations
- SourcePlanarUnweightedEquation.lean 1 declarations
- SubspaceTangentSupport.lean 4 declarations
- SupportDescendantCountable.lean 1 declarations
- TwoSidedIntrinsicDensity.lean 6 declarations
- UniformBilateralExcessPropagation.lean 2 declarations
- UniformDistanceTransfer.lean 1 declarations
- UniformExcessPropagation.lean 1 declarations
- UnweightedCappedEquation.lean 1 declarations
- VitaliLocalMassCharge.lean 1 declarations