OAI/MeasureTheory/Falconer/Measures/
350 declarations, 0 contain sorry, 0 declared as axioms; 116 files
Files
- AmbientMaskProductBudget.lean 2 declarations
- AmbientProduct.lean 8 declarations
- BorelProductPartition.lean 4 declarations
- BoundedDualDensity.lean 1 declarations
- BudgetedEndpointProduct.lean 1 declarations
- CellRefinementMass.lean 1 declarations
- CellwiseCollisionPruning.lean 1 declarations
- ChartDensityEstimate.lean 1 declarations
- ChooseProjectedFrostman.lean 1 declarations
- ClassSupport.lean 5 declarations
- CollisionDensityCharge.lean 1 declarations
- CollisionPruningMultiplication.lean 2 declarations
- ComparableIntegralPartition.lean 1 declarations
- ComparableNormalization.lean 1 declarations
- ConditionalFrostman.lean 4 declarations
- CubeMass.lean 2 declarations
- CubeProbability.lean 2 declarations
- DenseNeighborPruning.lean 3 declarations
- DensityCellCharge.lean 1 declarations
- DensityTreeMultiplication.lean 1 declarations
- DensityTruncation.lean 10 declarations
- DescriptorProduct.lean 9 declarations
- DistanceMatrixSchur.lean 3 declarations
- DistanceMeasure.lean 8 declarations
- DistanceSchurIntegral.lean 1 declarations
- DistributionAbsoluteContinuity.lean 2 declarations
- DyadicIntegralSplitting.lean 5 declarations
- DyadicMeasure.lean 9 declarations
- DyadicMeasureSplitting.lean 2 declarations
- EndpointMassRatios.lean 3 declarations
- EndpointScaleProduct.lean 1 declarations
- ExceptionalFiberMass.lean 1 declarations
- ExtendedDensityNorm.lean 4 declarations
- FarOriginalSupport.lean 6 declarations
- FiberDensityPruning.lean 5 declarations
- FiniteLpIntegral.lean 1 declarations
- FiniteMassMultiplication.lean 2 declarations
- FiniteMeasureProducts.lean 2 declarations
- FiniteProductIntegral.lean 3 declarations
- FiniteRelativePruning.lean 1 declarations
- FirstExclusionMass.lean 4 declarations
- FourCellMeasureSplitting.lean 4 declarations
- FourSpatialPairMeasure.lean 4 declarations
- FrequencyMeasure.lean 8 declarations
- FrostmanDimension.lean 2 declarations
- FrostmanDischarge.lean 2 declarations
- FrostmanWeakLimit.lean 3 declarations
- InactiveBinIntegral.lean 1 declarations
- InverseSupport.lean 2 declarations
- LiftedProductPartition.lean 3 declarations
- LocalPruningGain.lean 1 declarations
- MaskProductBudget.lean 2 declarations
- MaskSupport.lean 2 declarations
- MeanProbability.lean 5 declarations
- MonotoneMeasureMass.lean 2 declarations
- MultiscaleCollisionMass.lean 1 declarations
- MultiscaleDensityPruning.lean 4 declarations
- NormAffineRemainder.lean 1 declarations
- NormalizedLeibnizAssignment.lean 3 declarations
- NormalizedProjectedFrostman.lean 1 declarations
- OriginalConditionalFrostman.lean 2 declarations
- OriginalCoverRestriction.lean 2 declarations
- PacketProductPower.lean 1 declarations
- PairCorePruning.lean 3 declarations
- PartitionMaskedMeasure.lean 3 declarations
- PopularSquareMass.lean 1 declarations
- PrefixMass.lean 7 declarations
- PreparedMeasure.lean 5 declarations
- ProductCellPartition.lean 2 declarations
- ProductMatrixSchur.lean 2 declarations
- ProductPartitionMask.lean 5 declarations
- ProductProjectionReduction.lean 1 declarations
- ProductRestrictionLoss.lean 2 declarations
- ProductSchurIntegral.lean 3 declarations
- ProjectedSupportPoints.lean 2 declarations
- RegularProductParameters.lean 1 declarations
- RegularProductPower.lean 1 declarations
- RegularizedMass.lean 3 declarations
- RepresentedPruning.lean 1 declarations
- RescaledScaleProduct.lean 1 declarations
- RootNormalizedCoefficients.lean 4 declarations
- RootNormalizedError.lean 2 declarations
- RootSimilarityMeasures.lean 7 declarations
- ScalarBunchProducts.lean 4 declarations
- ScalarBunchPruning.lean 1 declarations
- ScalarDensityInverse.lean 2 declarations
- ScalarDensityMassControl.lean 1 declarations
- ScalarDensityRadius.lean 2 declarations
- ScalarDensitySelection.lean 2 declarations
- ScalarDensityZoom.lean 1 declarations
- ScalarPrefixPruning.lean 7 declarations
- ScalarProductBalls.lean 6 declarations
- ScalarProductFrostman.lean 4 declarations
- ScalarProductInterpolation.lean 3 declarations
- ScalarPruningPreservation.lean 7 declarations
- ScalarSingleChildPruning.lean 3 declarations
- ScalarSmallZoomMass.lean 2 declarations
- ScalarSubsetMass.lean 4 declarations
- ScalarTaggedPruning.lean 2 declarations
- Schur.lean 3 declarations
- SecondProjectedFrostman.lean 1 declarations
- SeparatedSupport.lean 16 declarations
- SimilarityMeasures.lean 7 declarations
- SimultaneousProjectedFrostman.lean 1 declarations
- SpatialRestriction.lean 3 declarations
- StartingMeasures.lean 7 declarations
- SupportPairFilter.lean 5 declarations
- TestNormDensity.lean 1 declarations
- TestNormMeasurable.lean 2 declarations
- TestNormRepresentation.lean 1 declarations
- TotalVariation.lean 3 declarations
- WeakApproximation.lean 4 declarations
- WeakLimit.lean 4 declarations
- WeightedIntegralSquare.lean 2 declarations
- WideProductParameters.lean 1 declarations
- WideProductPower.lean 1 declarations