OAI/MeasureTheory/Falconer/Recursion/
834 declarations, 0 contain sorry, 0 declared as axioms; 212 files
Files
- ActualDistanceRecursionBound.lean 2 declarations
- ActualPolicyPayments.lean 3 declarations
- ActualProfileContact.lean 1 declarations
- ActualRecursiveProfile.lean 4 declarations
- ActualSuffixLocalBins.lean 1 declarations
- ActualSuffixReduction.lean 1 declarations
- AnchoredTriplePotential.lean 2 declarations
- BlockLeafCounts.lean 8 declarations
- BlockRegularization.lean 14 declarations
- BoundedPotentialCompact.lean 3 declarations
- BranchAnalyticSuccessors.lean 16 declarations
- BranchCounts.lean 17 declarations
- BranchErrorBounds.lean 10 declarations
- BranchExponent.lean 1 declarations
- BranchExponentAlgebra.lean 6 declarations
- BranchLedger.lean 5 declarations
- BranchPotential.lean 9 declarations
- BranchRecursionOrder.lean 3 declarations
- BranchRepresentativeCharges.lean 3 declarations
- BranchTransitions.lean 20 declarations
- BranchValidity.lean 3 declarations
- ContactDepths.lean 1 declarations
- ContactLossBudget.lean 7 declarations
- CriticalPotential.lean 1 declarations
- CriticalScalarPotential.lean 1 declarations
- CriticalTruncatedPotential.lean 1 declarations
- DescriptorGoodTransfer.lean 1 declarations
- DescriptorMaskFailure.lean 3 declarations
- DescriptorMaskSymmetry.lean 5 declarations
- DescriptorMasks.lean 11 declarations
- DimensionalBranchBounds.lean 17 declarations
- DirectPolicyWitness.lean 3 declarations
- DisplacementDepth.lean 2 declarations
- DyadicWindowInterpolation.lean 1 declarations
- EndpointContactGain.lean 1 declarations
- EndpointScaleWindow.lean 1 declarations
- Entry.lean 1 declarations
- FarProfileNormalization.lean 1 declarations
- FiniteCountingPotential.lean 7 declarations
- FiniteCriticalPotential.lean 4 declarations
- FiniteProjectionPotential.lean 3 declarations
- FrequencyIntervals.lean 5 declarations
- FrostmanProfiles.lean 6 declarations
- InheritedEligibleWitness.lean 2 declarations
- InheritedPolicyState.lean 7 declarations
- InitialProfileClass.lean 2 declarations
- InnerProfileGrid.lean 5 declarations
- InteriorPolicy.lean 16 declarations
- IntermediateProfiles.lean 6 declarations
- LeafMassBins.lean 12 declarations
- Ledger.lean 13 declarations
- LocalProfileCounts.lean 4 declarations
- LocalProfileRegularity.lean 2 declarations
- MinimalDescriptorLength.lean 4 declarations
- NonendpointContactGain.lean 1 declarations
- NonendpointScaleWindow.lean 1 declarations
- OrderedEndpointIntervals.lean 3 declarations
- OrderedProfileIntervals.lean 3 declarations
- OrderedProfilePower.lean 2 declarations
- OuterEntryGain.lean 1 declarations
- OuterRecursiveTransport.lean 4 declarations
- ParallelProfile.lean 5 declarations
- ParentBinFamily.lean 7 declarations
- ParentBinSelection.lean 5 declarations
- ParentCellGeometry.lean 3 declarations
- ParentConeGeometry.lean 5 declarations
- ParentConeSource.lean 4 declarations
- ParentDiscardedForm.lean 1 declarations
- ParentHFBridge.lean 2 declarations
- ParentInactiveRemoval.lean 1 declarations
- ParentProfileBounds.lean 1 declarations
- PlanarCriticalPotential.lean 3 declarations
- PlanarWeakDepth.lean 2 declarations
- PointRieszPotential.lean 5 declarations
- PolicyBranchCoefficients.lean 7 declarations
- PolicyDescriptors.lean 14 declarations
- PolicyFarSuccessors.lean 6 declarations
- PolicyInteriorInterval.lean 5 declarations
- PolicyRecursionBounds.lean 5 declarations
- PolicyTerminal.lean 1 declarations
- PolicyWeightedRecursion.lean 2 declarations
- Potential.lean 14 declarations
- PotentialBallBound.lean 2 declarations
- PotentialFrostman.lean 2 declarations
- PotentialPair.lean 1 declarations
- PotentialScale.lean 3 declarations
- PrefixBandAssembly.lean 1 declarations
- PrefixChildDropping.lean 2 declarations
- PrefixCounting.lean 10 declarations
- PrefixInverseSupremum.lean 2 declarations
- PrefixLowMaximum.lean 4 declarations
- PrefixMass.lean 8 declarations
- PrefixPolicyGeometry.lean 3 declarations
- ProductPrefixCount.lean 5 declarations
- ProductRetainedStrip.lean 5 declarations
- ProfileApplicationBudget.lean 3 declarations
- ProfileBalls.lean 5 declarations
- ProfileBetweenNodes.lean 3 declarations
- ProfileBlockRefinement.lean 1 declarations
- ProfileBranchCounts.lean 7 declarations
- ProfileCellFamily.lean 7 declarations
- ProfileChordBounds.lean 3 declarations
- ProfileCompactness.lean 6 declarations
- ProfileContactInterval.lean 2 declarations
- ProfileContactStability.lean 1 declarations
- ProfileDecomposition.lean 2 declarations
- ProfileEndpointBound.lean 7 declarations
- ProfileEndpointStability.lean 8 declarations
- ProfileEntry.lean 1 declarations
- ProfileEnvelopes.lean 3 declarations
- ProfileExcess.lean 4 declarations
- ProfileGainAccounting.lean 3 declarations
- ProfileGainParameters.lean 4 declarations
- ProfileGeometryBudget.lean 1 declarations
- ProfileGeometryPower.lean 3 declarations
- ProfileGoodBound.lean 1 declarations
- ProfileGrid.lean 11 declarations
- ProfileGridCells.lean 7 declarations
- ProfileGridThreshold.lean 1 declarations
- ProfileHighMass.lean 5 declarations
- ProfileIncrementFrostman.lean 2 declarations
- ProfileInterpolation.lean 14 declarations
- ProfileIntervalChain.lean 4 declarations
- ProfileIterationBudget.lean 2 declarations
- ProfileLipschitz.lean 3 declarations
- ProfileLoss.lean 4 declarations
- ProfileLowerBound.lean 1 declarations
- ProfileMergeStep.lean 1 declarations
- ProfileMerging.lean 1 declarations
- ProfileNear.lean 5 declarations
- ProfileNodeValues.lean 4 declarations
- ProfileNormalBound.lean 1 declarations
- ProfileNormalBudget.lean 3 declarations
- ProfilePacking.lean 3 declarations
- ProfilePairMass.lean 1 declarations
- ProfilePrefix.lean 6 declarations
- ProfileRestriction.lean 3 declarations
- ProfileRightContact.lean 2 declarations
- ProfileRoundContact.lean 2 declarations
- ProfileScaleInduction.lean 1 declarations
- ProfileScaleSelection.lean 1 declarations
- ProfileStepBudget.lean 4 declarations
- ProfileSuffixContact.lean 2 declarations
- ProfileSuffixMinimum.lean 5 declarations
- ProfileTelescoping.lean 6 declarations
- ProfileUniformIterationBudget.lean 1 declarations
- ProfileUniformLimit.lean 6 declarations
- ProjectionProfileAlgebra.lean 1 declarations
- ProjectionProfileMean.lean 1 declarations
- ReachedBranchWeights.lean 9 declarations
- ReachedStateRecursion.lean 11 declarations
- RecursiveCellInvariants.lean 9 declarations
- RegularPacketScaleBudget.lean 1 declarations
- RegularizedPotential.lean 1 declarations
- RelativeScaleBudget.lean 2 declarations
- RetainedPairMasks.lean 12 declarations
- RetainedProfileBounds.lean 4 declarations
- RoundedContactWidth.lean 1 declarations
- RoundedHighProfile.lean 2 declarations
- RoundedProfileContact.lean 2 declarations
- RoundedProfileError.lean 5 declarations
- RoundedProfileGain.lean 4 declarations
- RoundedProfilePieces.lean 2 declarations
- ScalarBinaryBranch.lean 7 declarations
- ScalarBranchAccounting.lean 5 declarations
- ScalarBranchGrowth.lean 3 declarations
- ScalarBranchingLevel.lean 3 declarations
- ScalarBunchingLedger.lean 7 declarations
- ScalarPotential.lean 1 declarations
- ScalarProductPotential.lean 1 declarations
- ScalarTerminalFiberMass.lean 1 declarations
- ScalarTerminalPorousGain.lean 1 declarations
- ScalarTerminalProjection.lean 1 declarations
- ScalarTerminalPruning.lean 2 declarations
- SourceBranchDepth.lean 6 declarations
- SourceClassContact.lean 1 declarations
- SourceClassIntervals.lean 1 declarations
- SourcePrefixReduction.lean 2 declarations
- SourceSuffixReduction.lean 1 declarations
- SuffixBinAssembly.lean 1 declarations
- SuffixBinGeometry.lean 3 declarations
- SuffixCoarseDomination.lean 3 declarations
- SuffixDescriptors.lean 4 declarations
- SuffixDirectionGeometry.lean 3 declarations
- SuffixDistanceTaylor.lean 2 declarations
- SuffixGoodTransport.lean 1 declarations
- SuffixLocalBins.lean 2 declarations
- SuffixNormalization.lean 4 declarations
- SuffixPowerLoss.lean 2 declarations
- SuffixRetainedPairs.lean 10 declarations
- SurfacePotential.lean 2 declarations
- ThreeIntervalCost.lean 1 declarations
- ThreeIntervalData.lean 6 declarations
- ThreeIntervalDyadicGain.lean 1 declarations
- ThreeIntervalPower.lean 1 declarations
- ThreeIntervalProduct.lean 2 declarations
- ThreeIntervalShift.lean 2 declarations
- TruncatedScalarPotential.lean 2 declarations
- TwoProfileEnergy.lean 3 declarations
- TwoProfileInverse.lean 1 declarations
- TwoProfileInverseCost.lean 2 declarations
- TwoProfileInverseIntegrable.lean 5 declarations
- TwoProfileInverseScalar.lean 2 declarations
- TwoProfileRecursion.lean 4 declarations
- TwoRootGain.lean 2 declarations
- UniformContactDepths.lean 1 declarations
- UniformFrostmanProfiles.lean 1 declarations
- UniformProfileContact.lean 2 declarations
- UniformProfileGain.lean 1 declarations
- UniformScaleBudgets.lean 4 declarations
- UnitProfiles.lean 7 declarations
- WeightedBranchInduction.lean 1 declarations