OAI/Analysis/RotationWeights/
1539 declarations, 0 contain sorry, 0 declared as axioms; 51 files
Files
- ActualDigits.lean 53 declarations
- BorelTransport.lean 8 declarations
- BorelWeights.lean 34 declarations
- Concentration.lean 50 declarations
- ConditionalBounds.lean 17 declarations
- ContinuousWeight.lean 14 declarations
- Convolution.lean 16 declarations
- CoordinateLaws.lean 46 declarations
- CouplingMoments.lean 22 declarations
- Covariance.lean 21 declarations
- CrossingEstimates.lean 33 declarations
- Decomposable.lean 14 declarations
- DigitCouplings.lean 51 declarations
- Discrepancy.lean 25 declarations
- EndpointMoments.lean 30 declarations
- FiberActions.lean 36 declarations
- Fibers.lean 20 declarations
- FieldExtraction.lean 14 declarations
- FiniteSampling.lean 22 declarations
- FourierSampling.lean 59 declarations
- FunctionalCalculus.lean 23 declarations
- GraphTransfer.lean 36 declarations
- LaurentCoefficients.lean 37 declarations
- LogarithmicDrops.lean 41 declarations
- Main.lean 18 declarations
- MaskedEstimates.lean 6 declarations
- MeasurableWeight.lean 51 declarations
- Model.lean 10 declarations
- NestedAngles.lean 50 declarations
- OrbitBounds.lean 68 declarations
- Parameters.lean 52 declarations
- PhaseWeights.lean 41 declarations
- Polar.lean 29 declarations
- ProductSampling.lean 29 declarations
- ProjectionFields.lean 11 declarations
- ProjectionIdentity.lean 12 declarations
- RadixDigits.lean 54 declarations
- RationalGraphs.lean 32 declarations
- Regular.lean 33 declarations
- ReturnSamples.lean 16 declarations
- Rounding.lean 36 declarations
- SamplingBounds.lean 39 declarations
- SamplingStage.lean 21 declarations
- TaggedEvents.lean 32 declarations
- TailBounds.lean 24 declarations
- TensorBasis.lean 17 declarations
- Thresholds.lean 30 declarations
- TracialAction.lean 26 declarations
- Transport.lean 25 declarations
- TrialBounds.lean 17 declarations
- WeakSampling.lean 38 declarations