OAI/Analysis/IrrationalRotation/Couplings/
426 declarations, 0 contain sorry, 0 declared as axioms; 68 files
Files
- BiasedTailDensity.lean 11 declarations
- BlockProductCoupling.lean 11 declarations
- BlockedCouplingDensity.lean 4 declarations
- BlockedCouplingEnergy.lean 3 declarations
- BlockedProductCoupling.lean 10 declarations
- CircleConditionalAttenuation.lean 7 declarations
- CircleConditionalConvolutionData.lean 1 declarations
- CircleConditionalLabels.lean 2 declarations
- CircleConditionalProbabilities.lean 2 declarations
- CircleCoupling.lean 1 import, no declarations
- CircleCouplingAttenuation.lean 2 declarations
- CircleCouplingCocycleLaws.lean 3 declarations
- CircleCouplingConditioning.lean 6 declarations
- CircleCouplingCrossings.lean 4 declarations
- CircleCouplingDisintegration.lean 2 declarations
- CircleCouplingForcing.lean 6 declarations
- CircleCouplingHybrid.lean 11 declarations
- CircleCouplingLaw.lean 9 declarations
- CircleCouplingNonterminal.lean 3 declarations
- CircleCouplingOrder.lean 9 declarations
- CircleCouplingParameters.lean 6 declarations
- CircleCouplingSupport.lean 5 declarations
- CircleCouplingTagSupport.lean 5 declarations
- CircleDigitCoupling.lean 8 declarations
- ConditionalAvoidance.lean 12 declarations
- ConditionalConvolution.lean 13 declarations
- ConditionalConvolutionPointwise.lean 2 declarations
- ConditionalCrossingAvoidance.lean 7 declarations
- ConditionalDistributionEvents.lean 2 declarations
- ConditionalEndpointTransport.lean 1 declarations
- ConditionalEventBridge.lean 1 declarations
- ConditionalEventLocalization.lean 2 declarations
- ConditionalKernelSupport.lean 2 declarations
- ConditionalL2Tail.lean 5 declarations
- ConditionalMaskedTail.lean 1 declarations
- ConditionalObservationTransport.lean 4 declarations
- CouplingMarginalBounds.lean 20 declarations
- CouplingMixture.lean 25 declarations
- FiniteConditionalAttenuation.lean 5 declarations
- MixedRadixHybridLaw.lean 7 declarations
- OneCoordinateConditional.lean 5 declarations
- OneCoordinateCoupling.lean 19 declarations
- PrefixHybrid.lean 13 declarations
- PrefixPairIdentity.lean 1 declarations
- ProductBiasedIdentity.lean 2 declarations
- ProductBiasedIdentityFromTriangular.lean 3 declarations
- ProductBiasedPrefixTransfer.lean 1 declarations
- ProductCircleConditionalEvents.lean 1 declarations
- ProductCircleCrossingConditionalExpectation.lean 4 declarations
- ProductConditionalAttenuation.lean 5 declarations
- ProductConditionalCrossing.lean 4 declarations
- ProductConditionalData.lean 6 declarations
- ProductConditionalEvents.lean 5 declarations
- ProductConditionalKernels.lean 10 declarations
- ProductConditionalThresholds.lean 3 declarations
- ProductCoupling.lean 17 declarations
- ProductCouplingCircle.lean 22 declarations
- ProductCouplingCircleSource.lean 5 declarations
- ProductCouplingCocycleAttenuation.lean 1 declarations
- ProductCouplingCocycleBounds.lean 3 declarations
- ProductCouplingPrefix.lean 6 declarations
- ProductCrossingConditionalExpectation.lean 5 declarations
- ProductDensity.lean 18 declarations
- ProductDensityLimit.lean 15 declarations
- ProductPairIdentity.lean 1 declarations
- ProductPrefixConditionalLaw.lean 7 declarations
- ProductSourceConditionalData.lean 4 declarations
- SourceCouplingMarginals.lean 1 declarations