OAI/Analysis/RieszRectifiability/Kernel/
669 declarations, 0 contain sorry, 0 declared as axioms; 175 files
Files
- ADTruncations.lean 3 declarations
- AnchorPerturbation.lean 4 declarations
- ApproximationComparison.lean 3 declarations
- BallLocalization.lean 6 declarations
- BlowupNormalMomentDecay.lean 1 declarations
- BlowupNormalMoments.lean 6 declarations
- BlowupRieszOperator.lean 6 declarations
- BlowupScalarPairing.lean 5 declarations
- BoundedBoxBoundary.lean 6 declarations
- BoundedBoxContainment.lean 6 declarations
- BoundedBoxHeight.lean 3 declarations
- BoundedGlobalHeight.lean 1 declarations
- BoundedRegionTests.lean 8 declarations
- CapErrorBilinear.lean 1 declarations
- CappedBilinearError.lean 2 declarations
- CappedBilinearKernel.lean 11 declarations
- CappedBilinearL2.lean 1 declarations
- CappedDensityPairing.lean 1 declarations
- CappedEnergy.lean 9 declarations
- CappedMeanZeroTail.lean 2 declarations
- CappedPairingSymmetrization.lean 3 declarations
- CappedRieszInterior.lean 6 declarations
- CappedRieszKernel.lean 12 declarations
- CenteredShellMoments.lean 4 declarations
- ClosedTailBounds.lean 5 declarations
- CommonFiniteTruncation.lean 1 declarations
- CommonHeightEquation.lean 1 declarations
- CommonHeightLocalIntegrability.lean 2 declarations
- CommonHeightPolynomial.lean 2 declarations
- ComplexExteriorIntegrability.lean 3 declarations
- ComplexHeightPairing.lean 6 declarations
- ComplexInteriorEnergy.lean 3 declarations
- ComplexPairingRealComponents.lean 5 declarations
- CorrectedSingularTests.lean 3 declarations
- CountableLocalization.lean 1 declarations
- CutoffEnergyIntegral.lean 6 declarations
- CutoffError.lean 3 declarations
- CutoffTestMoments.lean 3 declarations
- DensityRieszTransforms.lean 3 declarations
- DerivativeTests.lean 3 declarations
- DyadicAnnuli.lean 7 declarations
- DyadicBoxes.lean 17 declarations
- DyadicCommonHeightEquation.lean 1 declarations
- DyadicMomentAllRadii.lean 2 declarations
- DyadicSourceMoments.lean 3 declarations
- DyadicSourceTails.lean 4 declarations
- EnergyFromTruncations.lean 5 declarations
- EnergyIdentity.lean 4 declarations
- EuclideanCoordinateMoments.lean 3 declarations
- ExpandingSmoothCutoffs.lean 7 declarations
- ExteriorDilation.lean 3 declarations
- ExteriorDilationIntegrability.lean 3 declarations
- FarHeightTail.lean 3 declarations
- FarKernelDifference.lean 2 declarations
- FarRieszTransform.lean 5 declarations
- FarTestKernelBounds.lean 5 declarations
- FiniteRieszPairing.lean 11 declarations
- FiniteShellTail.lean 5 declarations
- FiniteStepLp.lean 6 declarations
- FiniteStepMoments.lean 10 declarations
- GlobalGrowth.lean 3 declarations
- GlobalSingularHeight.lean 1 declarations
- GradientRieszTestIdentity.lean 4 declarations
- HardBilinearPairing.lean 4 declarations
- HeightEnergyPairingIdentity.lean 1 declarations
- HeightPairingExhaustion.lean 3 declarations
- HeightPairingRegions.lean 8 declarations
- HeightTailSplit.lean 5 declarations
- HomogeneousExteriorVanishing.lean 1 declarations
- InfiniteHeightTail.lean 4 declarations
- InheritedDyadicTail.lean 1 declarations
- InheritedHeightMoments.lean 3 declarations
- InheritedHeightTail.lean 1 declarations
- InnerAnnuli.lean 8 declarations
- InnerEnergyRestriction.lean 1 declarations
- IntrinsicHeightData.lean 6 declarations
- IsometricRieszPairing.lean 5 declarations
- KernelBasic.lean 7 declarations
- KernelNear.lean 4 declarations
- KernelTails.lean 3 declarations
- KernelTestSupport.lean 2 declarations
- L2Pairings.lean 6 declarations
- LeastSquaredExcess.lean 9 declarations
- LinearCoordinateFactorization.lean 1 declarations
- LipschitzL2Density.lean 3 declarations
- LipschitzRetractionError.lean 2 declarations
- LipschitzTests.lean 4 declarations
- LocalHeightData.lean 1 declarations
- LocalLipschitzEnergy.lean 7 declarations
- LocalRenormalizedRepresentative.lean 2 declarations
- LocalSchwartzSecondDifference.lean 3 declarations
- LocalTestMoments.lean 2 declarations
- LocalizedNormalTest.lean 4 declarations
- LocalizedRieszPairingBounds.lean 4 declarations
- MeanCorrectionAdmissible.lean 3 declarations
- MeanZero.lean 4 declarations
- MeanZeroFarTestEstimate.lean 1 declarations
- MeanZeroGramDecay.lean 5 declarations
- MeanZeroSchwartzApproximation.lean 5 declarations
- MomentRepair.lean 2 declarations
- NativeTruncationDecomposition.lean 2 declarations
- NearBilinear.lean 2 declarations
- NearPairWeight.lean 10 declarations
- NearSupportMassCharge.lean 1 declarations
- NonconcentrationPoint.lean 3 declarations
- NormalAnnularKernel.lean 4 declarations
- NormalCoordinateMoments.lean 1 declarations
- NormalCoordinateTests.lean 7 declarations
- NormalPairingEnergy.lean 4 declarations
- NormalizedBumpPairings.lean 4 declarations
- NormalizedEnergy.lean 4 declarations
- NormalizedExteriorPairing.lean 3 declarations
- NormalizedNormalCoordinates.lean 7 declarations
- NormalizedTailDecay.lean 3 declarations
- OpenOverlapCutoff.lean 2 declarations
- OrderedSpanConditioning.lean 6 declarations
- OriginalTestCutoffError.lean 3 declarations
- OscillationEnergy.lean 4 declarations
- OscillationTests.lean 7 declarations
- OuterCutoffError.lean 1 declarations
- OverlapCompatibility.lean 3 declarations
- PairingLocalizationIndependence.lean 6 declarations
- PartitionEnergy.lean 6 declarations
- PartitionSecondMoments.lean 4 declarations
- PolynomialDecayBounds.lean 1 declarations
- PolynomialDegreeDrop.lean 2 declarations
- PolynomialHomogeneousScaling.lean 3 declarations
- PolynomialLeadingExterior.lean 1 declarations
- PolynomialTailDecay.lean 2 declarations
- PolynomialTailDegreeOne.lean 1 declarations
- RegionOscillation.lean 3 declarations
- RegionTailDecay.lean 1 declarations
- RenormalizedFarPairing.lean 5 declarations
- RestrictedTruncationBounds.lean 2 declarations
- RieszExteriorAdjoint.lean 3 declarations
- RieszInteriorCapError.lean 2 declarations
- RieszPairingIdentification.lean 11 declarations
- RieszPairingMeanCorrection.lean 5 declarations
- ScalarRieszLocalBound.lean 4 declarations
- ScalarRieszSpatialDomination.lean 1 declarations
- ScalarRieszTestBounds.lean 4 declarations
- SchwartzFirstMomentTails.lean 3 declarations
- SchwartzNormDivision.lean 5 declarations
- SchwartzPairingSeparation.lean 4 declarations
- SchwartzSecondDifference.lean 5 declarations
- SchwartzSupportLocalization.lean 3 declarations
- ShellHeightL1.lean 3 declarations
- ShiftedHeightTail.lean 2 declarations
- ShrinkingSchwartzLocalization.lean 9 declarations
- ShrinkingSmoothCutoffs.lean 7 declarations
- SourceDensityRieszEquation.lean 1 declarations
- SourceNormalizedMoments.lean 2 declarations
- SourceRadialCutoffMass.lean 2 declarations
- SpanCoefficientControl.lean 4 declarations
- StepPairings.lean 3 declarations
- SubtractedFarTestEstimate.lean 1 declarations
- SupportedExteriorPairing.lean 4 declarations
- SupportedKernelDecomposition.lean 3 declarations
- SymmetricHeightKernel.lean 3 declarations
- SymmetricKernelL2.lean 2 declarations
- SymmetricPairingSplit.lean 4 declarations
- TailBounds.lean 2 declarations
- TestStepApproximation.lean 3 declarations
- TranslatedFarTestIntegral.lean 3 declarations
- TranslatedRieszAnnuli.lean 1 declarations
- TruncationIntegrability.lean 4 declarations
- TruncationLinear.lean 8 declarations
- UncenteredEnergy.lean 2 declarations
- UniformBallMoments.lean 1 declarations
- UniformHeightTail.lean 3 declarations
- UniformNearBilinear.lean 1 declarations
- VectorKernelFarDifference.lean 4 declarations
- VectorL2PairingBounds.lean 2 declarations
- VectorNormalizedEnergy.lean 2 declarations
- WeightedCentering.lean 6 declarations