OAI/Probability/SwitchChain/
2202 declarations, 0 contain sorry, 0 declared as axioms; 222 files
Files
- ActualTripleSquare.lean 1 declarations
- AugmentedMatrixEquiv.lean 9 declarations
- BalancedBlockVariance.lean 10 declarations
- BinaryAssignments.lean 10 declarations
- BinaryColumnPartitions.lean 15 declarations
- Cardinality.lean 1 declarations
- CellProjectionTransport.lean 20 declarations
- CenteredKernelEvolution.lean 5 declarations
- CountCDF.lean 23 declarations
- CountCoupling.lean 20 declarations
- CountCovering.lean 11 declarations
- CountEigenEquation.lean 3 declarations
- CountEigenvalue.lean 8 declarations
- CrossCellAffineComposition.lean 5 declarations
- CrossCellAssignments.lean 14 declarations
- CrossCellConditionalExpectation.lean 5 declarations
- CrossCellIndependence.lean 6 declarations
- CrossCellMoments.lean 24 declarations
- CrossCellProjectionIndependence.lean 5 declarations
- CrossCovariance.lean 11 declarations
- CrossIndependent.lean 13 declarations
- CrossMatrix.lean 23 declarations
- CrossToggleCells.lean 4 declarations
- CrossToggleGain.lean 15 declarations
- CrossToggleGainFacts.lean 3 declarations
- CrossTogglePairs.lean 29 declarations
- Definitions.lean 28 declarations
- DisjointAlgebra.lean 5 declarations
- DisjointBlockGraph.lean 16 declarations
- DisjointBoundary.lean 11 declarations
- DisjointCellCounting.lean 20 declarations
- DisjointCellGlobal.lean 4 declarations
- DisjointCellGraph.lean 12 declarations
- DisjointConditionalRange.lean 5 declarations
- DisjointCoordinateFeasibility.lean 3 declarations
- DisjointCrossCellEquiv.lean 15 declarations
- DisjointDegreeCell.lean 3 declarations
- DisjointEncoding.lean 17 declarations
- DisjointEqualityFlags.lean 11 declarations
- DisjointFiberCell.lean 4 declarations
- DisjointFiberCoordinates.lean 6 declarations
- DisjointGraphAffine.lean 8 declarations
- DisjointIndicators.lean 11 declarations
- DisjointInternal.lean 7 declarations
- DisjointMomentBridge.lean 16 declarations
- DisjointPairAggregation.lean 2 declarations
- DisjointPairLabels.lean 3 declarations
- DisjointPairOrdering.lean 1 declarations
- DisjointProjectionCell.lean 12 declarations
- DisjointRealization.lean 17 declarations
- DisjointReconstruct.lean 19 declarations
- DisjointStateCell.lean 3 declarations
- DisjointStateCoordinates.lean 10 declarations
- DisjointStateExpectation.lean 9 declarations
- DisjointStateLaw.lean 20 declarations
- Energy.lean 11 declarations
- EnergyTransfer.lean 2 declarations
- FiberLabelCounting.lean 8 declarations
- FiberPairIndex.lean 9 declarations
- FiniteCellProjection.lean 14 declarations
- FiniteConnectivity.lean 1 declarations
- FiniteCountTransport.lean 9 declarations
- FiniteEventVectors.lean 17 declarations
- FiniteKernelAlgebra.lean 8 declarations
- FiniteKernelTV.lean 14 declarations
- FiniteObservableGeometry.lean 20 declarations
- FiniteVarianceDecomposition.lean 10 declarations
- FiniteVarianceEuclidean.lean 4 declarations
- FixedBlockCount.lean 9 declarations
- FixedBlockMarginal.lean 18 declarations
- FixedBlockPartitions.lean 14 declarations
- FixedBlockVariance.lean 16 declarations
- ForcedColumns.lean 21 declarations
- FourVertexSwitch.lean 14 declarations
- FrameSynthesis.lean 20 declarations
- FrozenRows.lean 9 declarations
- GapConnectivity.lean 2 declarations
- GramComparison.lean 5 declarations
- HavelConnectivity.lean 5 declarations
- HavelInduction.lean 6 declarations
- IndependentCell.lean 7 declarations
- IndependentMomentProjection.lean 2 declarations
- IndependentProjectionInteraction.lean 5 declarations
- InitialTV.lean 4 declarations
- InitialTVGraph.lean 5 declarations
- InvariantEnergyVariance.lean 6 declarations
- KernelNormalization.lean 4 declarations
- LocalGapEndgame.lean 2 declarations
- Main.lean 3 declarations
- MainFromGap.lean 1 declarations
- MatchingCount.lean 18 declarations
- MatrixRowVariance.lean 8 declarations
- MixingArithmetic.lean 3 declarations
- MixingTimeFromTV.lean 4 declarations
- NeighborAlignment.lean 1 declarations
- NumericMixing.lean 3 declarations
- OrthogonalPairResampling.lean 38 declarations
- PairActualAffine.lean 4 declarations
- PairAffineInteraction.lean 6 declarations
- PairAggregation.lean 9 declarations
- PairArrayEncoding.lean 13 declarations
- PairArraySlice.lean 4 declarations
- PairAssignmentMoves.lean 3 declarations
- PairCellProjection.lean 8 declarations
- PairComparisonEndpoint.lean 2 declarations
- PairCrossToggleTransport.lean 7 declarations
- PairDisjointAssembly.lean 2 declarations
- PairDisjointBudget.lean 2 declarations
- PairEqualityBudget.lean 17 declarations
- PairEqualityBudgetUnordered.lean 6 declarations
- PairEqualityCell.lean 4 declarations
- PairEqualityErrorLine.lean 13 declarations
- PairEqualityInactive.lean 6 declarations
- PairEqualityLocalization.lean 8 declarations
- PairEqualityOrientation.lean 14 declarations
- PairEqualityProjection.lean 19 declarations
- PairEqualityProjectionFacts.lean 19 declarations
- PairEqualityRestriction.lean 8 declarations
- PairEqualitySlice.lean 8 declarations
- PairEqualityUnordered.lean 16 declarations
- PairEqualityUnorderedSum.lean 4 declarations
- PairFiber.lean 32 declarations
- PairFiberBridge.lean 6 declarations
- PairFiberConnectivity.lean 4 declarations
- PairFiberDegree.lean 8 declarations
- PairFiberEnergy.lean 7 declarations
- PairFiberEqualityTransport.lean 9 declarations
- PairFiberEquiv.lean 13 declarations
- PairFiberOrientation.lean 11 declarations
- PairFiberRedundancy.lean 3 declarations
- PairFiberSliceComparison.lean 9 declarations
- PairFiberTransport.lean 12 declarations
- PairFibers.lean 32 declarations
- PairGeneratorSquare.lean 5 declarations
- PairInternalRedundancy.lean 5 declarations
- PairLocalComparison.lean 3 declarations
- PairOrbit.lean 10 declarations
- PairPoincare.lean 3 declarations
- PairProjectionCell.lean 15 declarations
- PairRangeInteraction.lean 1 declarations
- PairSquaredEnergy.lean 8 declarations
- PairSwapFlip.lean 8 declarations
- PairSwapFlipProjection.lean 5 declarations
- PairSwapInactive.lean 5 declarations
- PairSwapInactiveFlip.lean 4 declarations
- PairSwapInjectivity.lean 5 declarations
- PairSwitchComparison.lean 2 declarations
- PairTradeSwitch.lean 11 declarations
- PairTripleBridge.lean 3 declarations
- PermutationFactors.lean 4 declarations
- PermutationGenerator.lean 10 declarations
- PermutationPathComparison.lean 8 declarations
- PermutationPoincare.lean 9 declarations
- Prelude.lean 1 import, no declarations
- ProjectionRangeInteraction.lean 5 declarations
- ProjectionTools.lean 8 declarations
- ProposalLaplacian.lean 5 declarations
- ProposalUniqueness.lean 12 declarations
- RankOneCentering.lean 8 declarations
- RankOneInteraction.lean 14 declarations
- RankOneRestriction.lean 4 declarations
- RowVarianceAssembly.lean 4 declarations
- SliceActualSynthesis.lean 7 declarations
- SliceBounds.lean 8 declarations
- SliceCardEncoding.lean 6 declarations
- SliceCoefficientAlgebra.lean 28 declarations
- SliceEquality.lean 15 declarations
- SliceEuclideanGenerator.lean 15 declarations
- SliceFrameProjection.lean 3 declarations
- SliceGenerator.lean 11 declarations
- SliceGeneratorEquality.lean 6 declarations
- SliceGeneratorSampling.lean 9 declarations
- SliceGramAction.lean 8 declarations
- SliceGramConstant.lean 5 declarations
- SliceGramOrbit.lean 11 declarations
- SliceGramProfile.lean 5 declarations
- SliceGramScalars.lean 3 declarations
- SliceImageNorm.lean 14 declarations
- SliceLinearNorm.lean 5 declarations
- SliceMoments.lean 40 declarations
- SliceNormalizedFamily.lean 19 declarations
- SliceOperatorComparison.lean 6 declarations
- SlicePathComparison.lean 7 declarations
- SlicePermutationAction.lean 15 declarations
- SliceProjectionComparison.lean 7 declarations
- SliceReindexedComparison.lean 10 declarations
- SliceSynthesis.lean 16 declarations
- SliceSynthesisAction.lean 3 declarations
- SliceSynthesisBounds.lean 3 declarations
- SpectralFromSquare.lean 4 declarations
- SwitchConnectivityFromGap.lean 2 declarations
- SwitchFlip.lean 34 declarations
- SwitchFoundations.lean 20 declarations
- SwitchInFiber.lean 4 declarations
- SwitchLaplacian.lean 7 declarations
- SwitchMultiplicity.lean 7 declarations
- SwitchPairFiber.lean 4 declarations
- SwitchTV.lean 5 declarations
- SwitchWitness.lean 5 declarations
- TVFromL2.lean 6 declarations
- ThreeVertexEncoding.lean 39 declarations
- Transfer.lean 5 declarations
- TransitiveAverage.lean 4 declarations
- TripleActualRowBound.lean 10 declarations
- TripleAugmentedMatrix.lean 8 declarations
- TripleCellSummation.lean 6 declarations
- TripleCellTransport.lean 30 declarations
- TripleCellVarianceGluing.lean 15 declarations
- TripleCountEigenvalue.lean 4 declarations
- TripleCountGram.lean 13 declarations
- TripleCountLaw.lean 25 declarations
- TripleFiberConditioning.lean 8 declarations
- TripleGraphEncoding.lean 18 declarations
- TripleInternalEncoding.lean 28 declarations
- TripleMatrixEncoding.lean 14 declarations
- TripleMatrixFinEquiv.lean 8 declarations
- TriplePairFiber.lean 17 declarations
- TripleProjectionBridge.lean 5 declarations
- TripleStateReindex.lean 19 declarations
- UnorderedPairSums.lean 3 declarations
- VariableBlockVariance.lean 13 declarations
- WeightedConditionalVariance.lean 24 declarations