OAI/Computability/DirectedFeedback/Games/
6235 declarations, 0 contain sorry, 0 declared as axioms; 80 files
Files
- A4IndexCount.lean 59 declarations
- A5ForwardIndex.lean 59 declarations
- A5Scalar.lean 88 declarations
- ActualAdviceSampling.lean 44 declarations
- ActualAdviceStochasticBridge.lean 74 declarations
- ActualAdviceUpper.lean 90 declarations
- ActualCanonical.lean 98 declarations
- AddressTupleBody.lean 145 declarations
- AddressTupleLoaded.lean 87 declarations
- AdviceLaw.lean 74 declarations
- AffineWitnessNormalization.lean 68 declarations
- AlphabetReduction.lean 131 declarations
- BlockOrientations.lean 78 declarations
- CanonicalAddress.lean 97 declarations
- CayleySampling.lean 84 declarations
- CayleySpectral.lean 103 declarations
- ChainRule.lean 71 declarations
- ChildLifts.lean 90 declarations
- Collision.lean 64 declarations
- CompletedSampling.lean 56 declarations
- ConditionalIncidences.lean 106 declarations
- CoordinateTransport.lean 51 declarations
- Decoder.lean 63 declarations
- DegreeCover.lean 63 declarations
- Derivatives.lean 63 declarations
- EqualityFiber.lean 52 declarations
- ExpanderFamily.lean 129 declarations
- Explicit.lean 136 declarations
- FieldArray.lean 74 declarations
- FinalParameters.lean 92 declarations
- FinishReduction.lean 98 declarations
- Game.lean 71 declarations
- Generator.lean 127 declarations
- GeneratorModel.lean 105 declarations
- GenericPolynomial.lean 42 declarations
- Genericity.lean 58 declarations
- Harmonic.lean 69 declarations
- InitialGraph.lean 160 declarations
- KMSAnalyticCodomainTransport.lean 55 declarations
- KMSAnalyticHybridEnergyFiber.lean 53 declarations
- KMSAnalyticHybridEnergyImageSplit.lean 68 declarations
- KMSAnalyticHybridEnergyMixed.lean 65 declarations
- KMSAnalyticHyperplaneExtensions.lean 56 declarations
- KMSAnalyticSmallTransport.lean 43 declarations
- KMSBasisComparisonFibers.lean 72 declarations
- KMSBasisComparisonPseudorandom.lean 77 declarations
- KMSBasisComparisonRetention.lean 56 declarations
- KMSKernelFiberDefs.lean 54 declarations
- KernelCardinality.lean 103 declarations
- LocalEquation.lean 92 declarations
- MatrixChartDegreeNeighbors.lean 65 declarations
- NaturalTransport.lean 47 declarations
- NonlinearRecurrence.lean 75 declarations
- Overlay.lean 95 declarations
- Parameters.lean 96 declarations
- PartnerFullSampling.lean 56 declarations
- PositiveMultiplier.lean 56 declarations
- PoweringFinalConstants.lean 100 declarations
- PoweringReach.lean 127 declarations
- Preprocessing.lean 110 declarations
- Product.lean 84 declarations
- ProductLaw.lean 54 declarations
- ProfileCorrection.lean 59 declarations
- QuestionMarginal.lean 59 declarations
- RowErasureSliceQuotient.lean 66 declarations
- RowErasureSliceUniform.lean 69 declarations
- RowErasureSlices.lean 84 declarations
- SelectedInformation.lean 69 declarations
- SelectedLikelihood.lean 47 declarations
- SharedSampling.lean 57 declarations
- SignaturePrepare.lean 74 declarations
- StageData.lean 71 declarations
- SubmoduleInterval.lean 76 declarations
- Target.lean 112 declarations
- TensorDomination.lean 57 declarations
- TestEmit.lean 70 declarations
- TupleBody.lean 59 declarations
- UniformReduction.lean 120 declarations
- UpperMobius.lean 67 declarations
- VisibleTransfer.lean 41 declarations