OAI/MeasureTheory/FalconerCompletion/Graphs/
692 declarations, 0 contain sorry, 0 declared as axioms; 76 files
Files
- AeOccupiedOriginal.lean 2 declarations
- AllMaskProductAdmissible.lean 6 declarations
- AllMaskProductAdmissible2.lean 4 declarations
- AmbientDescendants.lean 29 declarations
- AngularMoment.lean 25 declarations
- AngularMoment2.lean 12 declarations
- AngularMomentBoundedFactor.lean 3 declarations
- AssemblyPairCoefficientSum.lean 2 declarations
- AssemblyPairMass.lean 1 declarations
- AssemblyRootGraph.lean 1 declarations
- ComplexOfPositiveFinite.lean 8 declarations
- DiagonalBinMassLe.lean 27 declarations
- EuclideanPairDirection.lean 3 declarations
- FarPairDirectionMeasurable.lean 4 declarations
- FarPairError.lean 3 declarations
- FirstCoverBinAeCover.lean 6 declarations
- FourPairLintegralRegroup.lean 2 declarations
- GraphCapScaleInvCrude.lean 8 declarations
- GraphChildSquare.lean 16 declarations
- GraphChildrenHSplit.lean 15 declarations
- GraphConstOneJet.lean 3 declarations
- GraphDegrees.lean 23 declarations
- GraphDescendants.lean 28 declarations
- GraphFiniteCrossedEstimate.lean 1 declarations
- GraphFiniteCutoffEstimate.lean 2 declarations
- GraphFiniteCutoffEstimate2.lean 2 declarations
- GraphFiniteDirectEstimate.lean 2 declarations
- GraphFiniteHFBound.lean 9 declarations
- GraphFiniteHFBound2.lean 9 declarations
- GraphFixedAngularBudget.lean 12 declarations
- GraphFixedSpatialTerm.lean 9 declarations
- GraphHFFiniteJetEstimate.lean 1 declarations
- GraphJetMul.lean 14 declarations
- GraphPerp.lean 13 declarations
- GraphPerp2.lean 13 declarations
- GraphRetainedDirect.lean 11 declarations
- GraphSourceFixedGeometry.lean 2 declarations
- GraphSourceFourSpatialDecay.lean 1 declarations
- GraphSymbolJetConj.lean 3 declarations
- IntegrableListSum.lean 5 declarations
- IntervalRamp.lean 36 declarations
- LawProbability.lean 6 declarations
- LiteralDyadicPaths.lean 8 declarations
- NearGrid.lean 9 declarations
- NormIteratedFDerivSmoothStar.lean 13 declarations
- NormalizedAngularWord.lean 7 declarations
- NormalizedAngularWord2.lean 7 declarations
- OutgoingWeightedKernelNorm.lean 4 declarations
- PairAmbientGoodRadialIffDistanceGood.lean 7 declarations
- PairMaskProduct.lean 4 declarations
- ProfileChildCard.lean 14 declarations
- ProfileChildCard2.lean 2 declarations
- RadialCutoffMemOfNeZero.lean 12 declarations
- ResidualAngular.lean 18 declarations
- ResidualPairSourceSymbolEqScalarPair.lean 5 declarations
- RetainedCenterTests.lean 26 declarations
- ScalarPairSymbol.lean 12 declarations
- SharedBinSupportCollision.lean 19 declarations
- SmoothEval.lean 10 declarations
- SmoothFinsetProduct.lean 6 declarations
- SmoothFinsetProduct2.lean 6 declarations
- SmoothReciprocalNormCompBound.lean 3 declarations
- SphereAxisIntegralNormBoundGeneral.lean 7 declarations
- SphereAxisIntegralZero.lean 7 declarations
- SphereAxisSmoothIntegrable.lean 5 declarations
- SpherePairFarSupported.lean 1 declarations
- SpherePairRadialCoefficient.lean 12 declarations
- SpherePlaneWaveSub.lean 18 declarations
- SpherePlaneWaveSub2.lean 12 declarations
- SpherePlaneWaveSub3.lean 3 declarations
- StartingPairFiltersTransport.lean 7 declarations
- SuffixDescendants.lean 23 declarations
- SymbolFiniteProductDerivative.lean 6 declarations
- SymbolFiniteProductDerivative2.lean 6 declarations
- TestedCellFamily.lean 5 declarations
- WeightLeafLabel.lean 6 declarations