OAI/MeasureTheory/Falconer/Incidence/
320 declarations, 0 contain sorry, 0 declared as axioms; 123 files
Files
- AngularTubeCount.lean 8 declarations
- BadRowIncidence.lean 1 declarations
- BlockCellGoodGain.lean 1 declarations
- BlockCellNormalGain.lean 3 declarations
- BlockCellNormalPower.lean 1 declarations
- BlockCellPower.lean 3 declarations
- BlockChordGeometry.lean 1 declarations
- BlockChordRegularity.lean 2 declarations
- BlockClassRatios.lean 1 declarations
- BlockDepthBracket.lean 1 declarations
- BlockDescendantCounts.lean 1 declarations
- BlockGrid.lean 4 declarations
- BlockIntervalLengths.lean 3 declarations
- BlockLeafCounts.lean 8 declarations
- BlockPrefixBallBound.lean 3 declarations
- BlockPrefixRetention.lean 1 declarations
- BlockProfileBallBound.lean 2 declarations
- BlockProfileCells.lean 5 declarations
- BlockProfileCover.lean 1 declarations
- BlockRegularization.lean 14 declarations
- BoundedFrozenHeavyCover.lean 1 declarations
- CenteredPacketPencils.lean 1 declarations
- CenteredPlanarIncidence.lean 1 declarations
- CoarseCellPencils.lean 1 declarations
- CoarsePacketGain.lean 1 declarations
- CoarsePacketParameters.lean 1 declarations
- CoarsePacketPoints.lean 2 declarations
- CoarsePencilSize.lean 3 declarations
- CoarsePencilWeights.lean 7 declarations
- CoarseSquashedPencils.lean 2 declarations
- CoarserPencilDirections.lean 1 declarations
- CommonTripleIncidence.lean 4 declarations
- CommonTubeCount.lean 1 declarations
- CommonTupleIncidence.lean 5 declarations
- ComparableFrozenPencils.lean 1 declarations
- CriticalPencilIncidence.lean 3 declarations
- CubicIncidence.lean 2 declarations
- FinerPencilDirections.lean 1 declarations
- FiniteBallBounds.lean 3 declarations
- FiniteBallPruning.lean 6 declarations
- FiniteLatticeLoomis.lean 2 declarations
- FiniteLoomisWhitney.lean 1 declarations
- FrozenCoarseConfiguration.lean 1 declarations
- FrozenCoarseObstruction.lean 1 declarations
- FrozenHeavyCover.lean 2 declarations
- FrozenPacketProduct.lean 1 declarations
- FrozenPacketRegularity.lean 1 declarations
- FrozenPacketSelection.lean 2 declarations
- FrozenPacketUpper.lean 2 declarations
- GoodPencilDirections.lean 2 declarations
- GoodProfileIncidence.lean 1 declarations
- GridCount.lean 7 declarations
- IncidenceBucketBudget.lean 2 declarations
- IncidenceMoment.lean 2 declarations
- IncidencePowerBudget.lean 3 declarations
- IncidenceProductChain.lean 4 declarations
- IncidenceSamples.lean 2 declarations
- IncidenceSampling.lean 3 declarations
- IncidenceScaleChoice.lean 1 declarations
- IncidentCoarsePencils.lean 1 declarations
- InterpolatedIncidence.lean 2 declarations
- InterpolatedPencilGain.lean 2 declarations
- LeafCenterIncidence.lean 2 declarations
- LeafIncidenceGain.lean 1 declarations
- LeafMassBins.lean 12 declarations
- LeafPencilTransport.lean 2 declarations
- LeafPrefixPower.lean 1 declarations
- LocalCellIncidence.lean 1 declarations
- LocalPencilPacketGain.lean 1 declarations
- LoomisWhitneyCoordinates.lean 5 declarations
- LoomisWhitneyThree.lean 1 declarations
- NormalProfileIncidence.lean 2 declarations
- NormalizedProductPencils.lean 11 declarations
- OriginalBlockIncidence.lean 1 declarations
- OriginalCoarsePackets.lean 1 declarations
- OriginalPencilEqualization.lean 1 declarations
- PacketRowPencils.lean 1 declarations
- ParentQuarterIncidence.lean 3 declarations
- PencilDirections.lean 4 declarations
- PencilEnergyPruning.lean 3 declarations
- PencilFiberEnergy.lean 5 declarations
- PencilGainAlgebra.lean 2 declarations
- PencilSecondMoment.lean 1 declarations
- PlanarBaselineIncidence.lean 1 declarations
- PlanarIncidence.lean 3 declarations
- PlanarLeafInjection.lean 6 declarations
- PowerIncidenceMass.lean 1 declarations
- ProfileBlockBudget.lean 1 declarations
- PublishedFurstenberg.lean 5 declarations
- PublishedLoomisWhitney.lean 2 declarations
- QuarterPencilGeometry.lean 6 declarations
- QuarterPencils.lean 6 declarations
- RadialBlockDepths.lean 9 declarations
- RadialBlockRadius.lean 2 declarations
- RadialIncidenceBound.lean 1 declarations
- RadialZoomFiniteBalls.lean 4 declarations
- RegularClassRadialIncidence.lean 2 declarations
- RegularCoarsePencils.lean 2 declarations
- RegularEnergyPencils.lean 4 declarations
- RegularProductIncidence.lean 1 declarations
- RegularizedTubePencils.lean 1 declarations
- RelativeBlockBallBound.lean 1 declarations
- RetainedCoarseIncidences.lean 1 declarations
- RoundedBlockIntervals.lean 3 declarations
- RoundedRowPencils.lean 12 declarations
- SampledFurstenberg.lean 1 declarations
- ScalarBlockPruning.lean 1 declarations
- ScalarBlockSumProduct.lean 1 declarations
- ScalarWeakBlockProjection.lean 1 declarations
- SquashedPencils.lean 5 declarations
- TransverseTubeCount.lean 1 declarations
- TroublesomeIncidence.lean 1 declarations
- TruncatedBlockBall.lean 1 declarations
- TruncatedBlockCover.lean 1 declarations
- TruncatedBlockRatio.lean 3 declarations
- UniformFrozenCells.lean 1 declarations
- UniformSmallCoverPencils.lean 1 declarations
- UpperBlockBracket.lean 1 declarations
- VariableBaselineIncidence.lean 2 declarations
- WeakCoarsePacketGain.lean 1 declarations
- WeightedLoomisBase.lean 3 declarations
- WeightedLoomisStep.lean 3 declarations
- WideProductIncidence.lean 1 declarations