`OAI/MeasureTheory/Falconer/Angular/`

1222 declarations, 0 contain sorry, 0 declared as axioms; 289 files

Files

ActualAngleMasks.lean 12 declarations
ActualAngularDropping.lean 2 declarations
ActualAngularEquation23.lean 1 declarations
ActualAngularNear.lean 1 declarations
ActualAngularNearDropping.lean 1 declarations
ActualAngularRecursionBound.lean 3 declarations
ActualAngularRegularization.lean 2 declarations
ActualAngularTerminal.lean 1 declarations
ActualAngularTests.lean 19 declarations
ActualFarCircleExpansion.lean 1 declarations
ActualFarStationaryReduction.lean 1 declarations
ActualFourStationarySupport.lean 1 declarations
ActualFullCircleStationary.lean 2 declarations
ActualInactiveCircle.lean 1 declarations
ActualSingleStationaryKernel.lean 3 declarations
ActualStationaryAmplitude.lean 2 declarations
ActualStationaryExpansion.lean 2 declarations
ActualStationaryProductKernel.lean 2 declarations
ActualStationarySpatialIntegrability.lean 1 declarations
ActualTwoPointStationary.lean 2 declarations
AllDimensionalAngularProfileSum.lean 3 declarations
AngleBumpScaling.lean 4 declarations
AngleCoordinateTests.lean 4 declarations
AngleMaskDerivatives.lean 6 declarations
AngleMaskPeriodicity.lean 3 declarations
AngularBinKernel.lean 11 declarations
AngularBinSelection.lean 7 declarations
AngularBootstrap.lean 2 declarations
AngularCellKernels.lean 4 declarations
AngularCellSpatialIntegral.lean 2 declarations
AngularChart.lean 6 declarations
AngularComparableCarrier.lean 1 declarations
AngularCountMean.lean 9 declarations
AngularDifferentialBounds.lean 5 declarations
AngularDifferentialExpr.lean 13 declarations
AngularDroppedMaximum.lean 3 declarations
AngularDyadicSum.lean 2 declarations
AngularEnergyDropping.lean 6 declarations
AngularEnvelope.lean 16 declarations
AngularEnvelopeGraph.lean 11 declarations
AngularFarDepth.lean 2 imports, no declarations
AngularFarGeometry.lean 2 declarations
AngularFarSeparation.lean 2 declarations
AngularFarSpatialSum.lean 1 declarations
AngularFarStationaryScale.lean 4 declarations
AngularFourCellMass.lean 6 declarations
AngularFourSpatialIntegral.lean 1 declarations
AngularGainFinite.lean 9 declarations
AngularGrid.lean 12 declarations
AngularIntegrability.lean 12 declarations
AngularIntegrationByParts.lean 7 declarations
AngularJetSymbol.lean 4 declarations
AngularKernelIntegral.lean 5 declarations
AngularLabelEligibility.lean 5 declarations
AngularLengthIntegralPartition.lean 2 declarations
AngularLengthPartition.lean 14 declarations
AngularMeanAssembly.lean 2 declarations
AngularNearIntegral.lean 1 declarations
AngularNearNeighbors.lean 4 declarations
AngularNearProfile.lean 2 declarations
AngularNearProgress.lean 2 declarations
AngularNearSum.lean 5 declarations
AngularNoncomparableCarrier.lean 1 declarations
AngularNonstationary.lean 2 declarations
AngularNonstationaryPower.lean 3 declarations
AngularOccupiedFarPartition.lean 2 declarations
AngularOccupiedPartition.lean 3 declarations
AngularOperatorTerms.lean 7 declarations
AngularOriginalFarPartition.lean 3 declarations
AngularOriginalIntegrability.lean 2 declarations
AngularPair.lean 5 declarations
AngularPairCircleIntegral.lean 4 declarations
AngularPairSwap.lean 1 declarations
AngularParentNearFar.lean 2 declarations
AngularProductEnergyIntegral.lean 9 declarations
AngularProfileSum.lean 3 declarations
AngularRadialKernel.lean 3 declarations
AngularRestrictedIntegralSum.lean 1 declarations
AngularRestrictedKernel.lean 4 declarations
AngularSamples.lean 8 declarations
AngularStateContributions.lean 9 declarations
AngularStateData.lean 13 declarations
AngularStateDropping.lean 2 declarations
AngularStateNearFar.lean 1 declarations
AngularStateSuccessor.lean 6 declarations
AngularStationaryRadialError.lean 5 declarations
AngularStationarySpatial.lean 8 declarations
AngularStripIntervals.lean 3 declarations
AngularStripMeasure.lean 5 declarations
AngularTerminal.lean 2 declarations
AngularTerminalBound.lean 1 declarations
AngularTransform.lean 2 declarations
AngularTransformSplitting.lean 5 declarations
AngularTransportBounds.lean 8 declarations
AngularTubeMean.lean 2 declarations
AngularTubes.lean 5 declarations
AngularUniformAbsorption.lean 2 declarations
AngularWidths.lean 9 declarations
BadDirectionEnvelope.lean 6 declarations
BadDirectionSelection.lean 1 declarations
CapAmplitudeDerivatives.lean 3 declarations
CapCoordinates.lean 1 declarations
CapCount.lean 2 declarations
CapCrossIntegral.lean 3 declarations
CapDenominator.lean 4 declarations
CapDensityCharge.lean 1 declarations
CapEnergyExpansion.lean 3 declarations
CapLocalization.lean 1 declarations
CapNet.lean 2 declarations
CapPairSymmetry.lean 2 declarations
CapReciprocal.lean 4 declarations
CapScaleGeometry.lean 2 declarations
CapSupport.lean 6 declarations
CapSymbolBounds.lean 1 declarations
CapTransport.lean 10 declarations
CappedActiveCover.lean 4 declarations
CappedOriginalCover.lean 2 declarations
CircleAngularBins.lean 11 declarations
CircleDirectCoefficients.lean 3 declarations
CircleLocalIntegral.lean 5 declarations
CircleMaskCoordinates.lean 12 declarations
CircleMaskSupport.lean 6 declarations
CircleResidualDecay.lean 1 declarations
CircleRotation.lean 12 declarations
CircleStationaryPartition.lean 11 declarations
CircleTests.lean 4 declarations
CommonProfileAngularNear.lean 1 declarations
CompactCircleResidual.lean 8 declarations
CompactStationaryAmplitude.lean 4 declarations
ControlledAngularGain.lean 1 declarations
ControlledCapPartition.lean 1 declarations
CubeCapacity.lean 11 declarations
DirectionDistance.lean 3 declarations
DiscardedCapTerm.lean 1 declarations
DyadicCapTerms.lean 3 declarations
DyadicLongitudinal.lean 1 declarations
DyadicPerpendicular.lean 1 declarations
EndpointAngularGain.lean 1 declarations
EndpointAngularParameters.lean 1 declarations
EndpointBadDirections.lean 1 declarations
EvenStartingCaps.lean 6 declarations
FactorizedAngularState.lean 11 declarations
FarAngularStep.lean 3 declarations
FiniteAngularSquare.lean 4 declarations
FlexibleAngularRoot.lean 2 declarations
FourPointCaps.lean 5 declarations
FourStationarySupport.lean 2 declarations
FullCircleDecomposition.lean 8 declarations
FullCircleStationaryExpansion.lean 3 declarations
FullCircleStationaryPower.lean 2 declarations
GlobalCapBounds.lean 10 declarations
GnomonicCap.lean 7 declarations
GnomonicChart.lean 17 declarations
GnomonicCone.lean 6 declarations
GnomonicConeVolume.lean 1 declarations
GnomonicDischarge.lean 2 declarations
GnomonicInverse.lean 22 declarations
GnomonicLaw.lean 2 declarations
GnomonicPairGram.lean 7 declarations
GnomonicPrunedLaw.lean 6 declarations
GnomonicTripleAngle.lean 5 declarations
GnomonicTripleKernel.lean 1 declarations
GoodDirectionMass.lean 1 declarations
GoodProjectionDirections.lean 4 declarations
GraphAngleCharts.lean 15 declarations
GraphAngularCoordinates.lean 7 declarations
GraphRotatedWeights.lean 10 declarations
GraphTorusAngles.lean 4 declarations
IneligibleCapTerms.lean 6 declarations
InheritedAngularSymbols.lean 8 declarations
InheritedCircleRegularity.lean 7 declarations
IntegerCaps.lean 4 declarations
InverseAngularSymbol.lean 2 declarations
InverseCircleArcLength.lean 9 declarations
InverseCircleAssembly.lean 4 declarations
InverseCirclePower.lean 1 declarations
InverseSphereFubini.lean 3 declarations
InverseStationaryCancellation.lean 2 declarations
InverseStationaryCutoff.lean 6 declarations
InverseStationaryOperators.lean 11 declarations
InverseStationaryRemainder.lean 3 declarations
InverseStationaryScales.lean 4 declarations
InverseStationaryTriangle.lean 2 declarations
InverseStationaryWeighted.lean 3 declarations
LocalDirectionPackets.lean 1 declarations
LocalizedStationaryExpansion.lean 3 declarations
LongitudinalCapTerm.lean 1 declarations
LongitudinalCrossTerm.lean 1 declarations
MeasurableAngularJets.lean 3 declarations
MixedCapBounds.lean 5 declarations
MixedCapDenominator.lean 1 declarations
MixedNormalizedCaps.lean 2 declarations
MultiscaleCapMass.lean 3 declarations
NoncomparableSphereKernel.lean 2 declarations
NonendpointAngularGain.lean 1 declarations
NonendpointBadDirections.lean 1 declarations
NormalizedCaps.lean 4 declarations
NormalizedStationaryJet.lean 3 declarations
NorthRotation.lean 14 declarations
OddAuxiliaryCaps.lean 2 declarations
OddOriginalCaps.lean 2 declarations
OriginalAngularKernel.lean 2 declarations
OriginalCapRemoval.lean 1 declarations
OriginalDirectionChart.lean 3 declarations
OriginalFiberCaps.lean 1 declarations
OuterAngularBound.lean 2 declarations
OuterAngularDecay.lean 1 declarations
PeriodicAngularBins.lean 10 declarations
PerpendicularCrossTerm.lean 1 declarations
PolicyAngularBranches.lean 10 declarations
ProjectedDirections.lean 3 declarations
ProjectionAngularGeometry.lean 5 declarations
ProjectionAngularMoment.lean 3 declarations
PublishedGnomonic.lean 4 declarations
PublishedIntegerCaps.lean 1 declarations
QuadraticStationaryExpansion.lean 5 declarations
QuadraticStationaryIdentity.lean 3 declarations
QuadraticStationaryL1.lean 4 declarations
QuantitativeCaps.lean 2 declarations
RadialStationaryProfile.lean 5 declarations
ReciprocalSineBounds.lean 3 declarations
RegularizedAngularNear.lean 1 declarations
RetainedAngularFailure.lean 4 declarations
RetainedSmallSphere.lean 4 declarations
ReverseCapsAllRadii.lean 1 declarations
RootStationaryScale.lean 3 declarations
RotatedActualInactive.lean 1 declarations
RotatedBinPartition.lean 3 declarations
RotatedCircleIntegral.lean 1 declarations
RotatedConeKernel.lean 11 declarations
RotatedGraphEligibility.lean 7 declarations
RotatedInverseCircle.lean 5 declarations
RotatedParallelCandidates.lean 2 declarations
RotatedScaleNonstationary.lean 2 declarations
ScalarAngularShell.lean 2 declarations
ScaledAngularTransport.lean 3 declarations
SelectedAngularBins.lean 7 declarations
SharedAngular.lean 5 declarations
SignedStationaryExpansion.lean 6 declarations
SignedStationaryJet.lean 2 declarations
SignedStationaryRadial.lean 3 declarations
SingleStationaryAngular.lean 3 declarations
SingleStationaryIntegral.lean 4 declarations
SingleStationaryRadial.lean 3 declarations
SmallGnomonicCap.lean 2 declarations
SmoothAngleMask.lean 10 declarations
SmoothCapPartition.lean 3 declarations
SmoothInverseSine.lean 4 declarations
SmoothRotatedCone.lean 4 declarations
SourceAngularDirect.lean 1 declarations
SourceAngularReduction.lean 1 declarations
SphereCapBound.lean 4 declarations
SphereCapBox.lean 5 declarations
SphereCapCenters.lean 1 declarations
SphereChartIntegral.lean 1 declarations
SphereFrequency.lean 2 declarations
SphereInverse.lean 5 declarations
SphereModel.lean 4 declarations
SphereNonstationary.lean 2 declarations
SphereNormalization.lean 5 declarations
SphereOffPole.lean 2 declarations
SphereProduct.lean 5 declarations
SphereRotations.lean 6 declarations
SphereStationary.lean 2 declarations
SphereStationaryAssembly.lean 9 declarations
StationaryApproximantSupport.lean 3 declarations
StationaryArcLength.lean 2 declarations
StationaryChartAmplitude.lean 6 declarations
StationaryChartCutoffs.lean 14 declarations
StationaryChartIntegral.lean 3 declarations
StationaryDifferentialExpr.lean 11 declarations
StationaryJetLocality.lean 5 declarations
StationaryJetOperators.lean 9 declarations
StationaryOppositePhase.lean 3 declarations
StationaryPairGain.lean 2 declarations
StationaryPairSupport.lean 5 declarations
StationaryPowerRate.lean 2 declarations
StationaryProductIntegral.lean 4 declarations
StationaryProductKernel.lean 1 declarations
StationaryRadialCoefficient.lean 3 declarations
StationaryRadialScaling.lean 2 declarations
StationaryRemainderScale.lean 3 declarations
StationarySineChart.lean 11 declarations
SuffixAngularRadius.lean 2 declarations
SuffixDirection.lean 4 declarations
TubeDirectionRobustness.lean 3 declarations
TwoProjectionIntegerCaps.lean 1 declarations
VectorSphereKernel.lean 3 declarations
WitnessDirection.lean 1 declarations