OAI/MeasureTheory/Falconer/Geometry/
837 declarations, 0 contain sorry, 0 declared as axioms; 230 files
Files
- ActiveCoverScale.lean 1 declarations
- AmbientChartBudget.lean 2 declarations
- BallTruncation.lean 4 declarations
- BinBands.lean 3 declarations
- BinEstimates.lean 5 declarations
- BinOffsets.lean 5 declarations
- Bins.lean 6 declarations
- BoundedChartFineGain.lean 1 declarations
- BoundedProjectionCoordinates.lean 10 declarations
- CellNormalization.lean 6 declarations
- CellNorthFrame.lean 1 declarations
- CellwiseDistanceForm.lean 6 declarations
- ChartCoordinates.lean 14 declarations
- ChartCostMeasurable.lean 2 declarations
- ChartFiniteScaleBounds.lean 2 declarations
- ChartFrame.lean 4 declarations
- ChartGainBudget.lean 1 declarations
- ChartGeometry.lean 3 declarations
- ChartNonstationary.lean 2 declarations
- ChartPairPower.lean 1 declarations
- ChartPairTransfer.lean 1 declarations
- ChooseNonchargingProjection.lean 1 declarations
- CommonNormalizedProjections.lean 2 declarations
- CommonProjectionConfiguration.lean 1 declarations
- CommonProjectionLosses.lean 2 declarations
- CommonRatioProjections.lean 1 declarations
- CommonRectangles.lean 1 declarations
- CommonSmallProjections.lean 1 declarations
- CommonUnbalancedProjections.lean 1 declarations
- CompactMultiplierScale.lean 1 declarations
- CompactQuadraticExpansion.lean 2 declarations
- CompactSublevel.lean 1 declarations
- ComparableCellCounting.lean 3 declarations
- ConditionalBalls.lean 3 declarations
- ConditionalCellGeometry.lean 1 declarations
- ConditionalProjectionBuffer.lean 2 declarations
- ConditionalProjectionTest.lean 5 declarations
- CubeBallBound.lean 2 declarations
- CubeBallPacking.lean 4 declarations
- DyadicBallCount.lean 3 declarations
- DyadicCenterSeparation.lean 2 declarations
- DyadicClasses.lean 19 declarations
- DyadicCube.lean 10 declarations
- DyadicGeometry.lean 10 declarations
- DyadicInverseDistance.lean 2 declarations
- DyadicPacking.lean 16 declarations
- DyadicScaleBallBounds.lean 2 declarations
- DyadicSeparation.lean 1 declarations
- EndpointChartGain.lean 1 declarations
- EndpointChartObstruction.lean 1 declarations
- EndpointChartRadius.lean 1 declarations
- EndpointChartSelection.lean 2 declarations
- EndpointMidscaleCover.lean 1 declarations
- EndpointNormalize.lean 2 declarations
- EuclideanBallNet.lean 1 declarations
- EuclideanCross.lean 9 declarations
- EuclideanLpTrace.lean 3 declarations
- EuclideanMollifier.lean 11 declarations
- EuclideanRieszEnergy.lean 6 declarations
- EuclideanTrace.lean 4 declarations
- EuclideanWeakApproximation.lean 4 declarations
- FactorChartControl.lean 2 declarations
- FarCellGeometry.lean 3 declarations
- FarNormalization.lean 2 declarations
- FarNormalizedBound.lean 2 declarations
- FiniteBinComparison.lean 3 declarations
- FinitePrefixBallBound.lean 2 declarations
- FinitePrefixCover.lean 1 declarations
- FiniteProjectionSublevels.lean 1 declarations
- FiniteScaleBall.lean 3 declarations
- FiniteWeightedProjectionSample.lean 1 declarations
- FixedChartBounds.lean 5 declarations
- FrameEmbedding.lean 4 declarations
- FrequencyGeometry.lean 3 declarations
- FullChartRegularGain.lean 1 declarations
- GeneralFrameBound.lean 3 declarations
- GeneralGridRounding.lean 7 declarations
- GeneralTransverseGrid.lean 2 declarations
- GridBallOverlap.lean 2 declarations
- GridProjectionTransfer.lean 5 declarations
- HalfSlopeGrid.lean 7 declarations
- InactiveBinDecay.lean 2 declarations
- InactiveBinGeometry.lean 7 declarations
- InactiveBinScales.lean 7 declarations
- IntegerBox.lean 2 declarations
- IntegerEnergyRefinement.lean 1 declarations
- IntegerFivePaths.lean 8 declarations
- IntegerFourPaths.lean 8 declarations
- IntegerMixedRefinement.lean 2 declarations
- IntegerRectangle.lean 3 declarations
- IntegerSumEnergy.lean 6 declarations
- LocalPointBalls.lean 2 declarations
- LocalPrefixCover.lean 2 declarations
- MaskedGeometry.lean 2 declarations
- MiddleScaleGeometry.lean 5 declarations
- NonendpointChartGain.lean 1 declarations
- NonstationaryGeometry.lean 7 declarations
- NormalSeparation.lean 1 declarations
- NormalizedDescriptorFamily.lean 2 declarations
- NormalizedGainBudget.lean 1 declarations
- NormalizedInverseFactors.lean 10 declarations
- NormalizedRegularGain.lean 1 declarations
- NormalizedSpatialFactors.lean 7 declarations
- NormalizedTripleGram.lean 2 declarations
- OccupiedCellSeparation.lean 3 declarations
- OneScaleGeometry.lean 6 declarations
- OrthonormalRectangle.lean 2 declarations
- ParentEndpointGeometry.lean 1 declarations
- PiCoordinateSections.lean 1 declarations
- PlanarChartRepair.lean 9 declarations
- PlanarGridCosts.lean 2 declarations
- PlanarGridRegularity.lean 1 declarations
- PlanarGridScales.lean 2 declarations
- PlanarProjectionCoordinates.lean 9 declarations
- PlanarScalarGrid.lean 13 declarations
- PlanarSlopeBalls.lean 10 declarations
- PointBallCounts.lean 3 declarations
- PolynomialNormalization.lean 1 declarations
- PositiveDistanceBins.lean 12 declarations
- ProfileGrid.lean 11 declarations
- ProjectedSeparation.lean 1 declarations
- ProjectionBuffer.lean 2 declarations
- ProjectionCells.lean 5 declarations
- ProjectionCollisionMean.lean 2 declarations
- ProjectionCoordinateBalls.lean 5 declarations
- ProjectionCube.lean 4 declarations
- ProjectionDilation.lean 5 declarations
- ProjectionEnergy.lean 5 declarations
- ProjectionExceptional.lean 1 declarations
- ProjectionGood.lean 4 declarations
- ProjectionKernel.lean 5 declarations
- ProjectionLaw.lean 7 declarations
- ProjectionPowerBudget.lean 2 declarations
- ProjectionRatioBounds.lean 2 declarations
- ProjectionRatioGeometry.lean 4 declarations
- ProjectionRatioRegularity.lean 1 declarations
- ProjectionRescaling.lean 1 declarations
- ProjectionRows.lean 10 declarations
- ProjectionSampleBudget.lean 6 declarations
- ProjectionSinc.lean 1 declarations
- QuadraticChart.lean 11 declarations
- QuadraticNormalization.lean 3 declarations
- QuarterChartFineGain.lean 1 declarations
- QuarterCoarseCover.lean 1 declarations
- RegularCoordinateRows.lean 1 declarations
- RegularSmallProjections.lean 2 declarations
- RelativeGridError.lean 4 declarations
- RelativePrefixBallBound.lean 3 declarations
- RetainedCoarseCover.lean 2 declarations
- RetainedEndpointGeometry.lean 1 declarations
- RobustProjectionSets.lean 3 declarations
- RootPatchGeometry.lean 5 declarations
- RootSimilarityGeometry.lean 12 declarations
- RoundedProjectionCoordinates.lean 8 declarations
- RowTubeBalls.lean 2 declarations
- SamplingGrid.lean 7 declarations
- ScalarBallCandidates.lean 7 declarations
- ScalarBoundedProjection.lean 1 declarations
- ScalarBunchGeometry.lean 4 declarations
- ScalarBunchNetGain.lean 2 declarations
- ScalarBunchProjection.lean 2 declarations
- ScalarClosureProjections.lean 1 declarations
- ScalarClusterProjection.lean 1 declarations
- ScalarCoverCount.lean 3 declarations
- ScalarCoverStability.lean 2 declarations
- ScalarDyadicGrid.lean 7 declarations
- ScalarDyadicProjection.lean 1 declarations
- ScalarForkGeometry.lean 2 declarations
- ScalarGeneratedGrid.lean 1 declarations
- ScalarGridFibers.lean 7 declarations
- ScalarGridGain.lean 3 declarations
- ScalarGridGainAlgebra.lean 2 declarations
- ScalarGridGainRates.lean 4 declarations
- ScalarGridGrouping.lean 2 declarations
- ScalarGridProjection.lean 2 declarations
- ScalarGridThinning.lean 3 declarations
- ScalarGroupGeometry.lean 2 declarations
- ScalarGroupReverseGeometry.lean 2 declarations
- ScalarGrowthOfCover.lean 1 declarations
- ScalarKernelGeometry.lean 4 declarations
- ScalarMaxRatioProjection.lean 1 declarations
- ScalarNetAmplification.lean 1 declarations
- ScalarNetIteration.lean 7 declarations
- ScalarNonporousCover.lean 3 declarations
- ScalarNormalizationCost.lean 4 declarations
- ScalarNormalizedCoefficients.lean 2 declarations
- ScalarNormalizedLogBudget.lean 4 declarations
- ScalarNormalizedProjection.lean 3 declarations
- ScalarPowerNet.lean 1 declarations
- ScalarProjectionComparison.lean 3 declarations
- ScalarProjectionDoubling.lean 2 declarations
- ScalarRationalProjection.lean 1 declarations
- ScalarRoundingBalls.lean 1 declarations
- ScalarRoundingCovers.lean 2 declarations
- ScalarRuzsaCovering.lean 1 declarations
- ScalarSmallSumCover.lean 1 declarations
- ScalarUniformProjection.lean 2 declarations
- ScalarUnitProjection.lean 1 declarations
- ScalarWeakProjection.lean 1 declarations
- ScalarWeakRadiusProjection.lean 1 declarations
- ScaledDyadicPacking.lean 5 declarations
- SeededSeparation.lean 7 declarations
- SelectTransverseChartTriple.lean 1 declarations
- SelectedBinAmplitude.lean 5 declarations
- SelectedChartGeometry.lean 3 declarations
- SelectedChartRelation.lean 3 declarations
- SeparatedDistanceMaximum.lean 5 declarations
- SeparatedProjectionBases.lean 1 declarations
- SeparatedSpatialDistanceForm.lean 1 declarations
- SeparationOrder.lean 12 declarations
- SimilarityGeometry.lean 11 declarations
- SmallChartCube.lean 6 declarations
- SquashCover.lean 1 declarations
- SurfaceTestNorm.lean 7 declarations
- TransverseGridCoordinates.lean 6 declarations
- TripleFrameBound.lean 4 declarations
- TripleGridRounding.lean 9 declarations
- TroublesomeCovers.lean 1 declarations
- TruncatedChordGeometry.lean 1 declarations
- TruncatedDyadicBalls.lean 1 declarations
- TubeAnchorNet.lean 4 declarations
- TubeFiberCoordinates.lean 4 declarations
- TwoNormalProjection.lean 1 declarations
- TwoPointTubeGeometry.lean 5 declarations
- TwoProjectionCubes.lean 2 declarations
- TwoProjectionFrame.lean 3 declarations
- TwoProjectionPiecePair.lean 6 declarations
- TwoProjectionPieces.lean 14 declarations
- UnbalancedRatioNormalization.lean 1 declarations
- UniformMiddleGeometry.lean 1 declarations