OAI/Probability/ParisiFinite/
6192 declarations, 0 contain sorry, 0 declared as axioms; 114 files
Files
- AbsMulExpLe.lean 46 declarations
- Act.lean 65 declarations
- ActualCenterPhase.lean 30 declarations
- ActualDisplacement.lean 43 declarations
- Average.lean 84 declarations
- BalancedConeEqForest.lean 66 declarations
- BoundedOf.lean 89 declarations
- BranchNumerator.lean 55 declarations
- CanonicalSpatialTest.lean 30 declarations
- ChildMomentLimit.lean 47 declarations
- Compatible.lean 54 declarations
- ContinuousTiltedMeanJoint.lean 17 declarations
- CoreScaleSqLeOne.lean 41 declarations
- CoshCone.lean 28 declarations
- CostState.lean 61 declarations
- Count.lean 70 declarations
- DyadicEvolutionGridBound.lean 55 declarations
- DyadicMeshTendsto.lean 62 declarations
- EmpiricalExpLog.lean 39 declarations
- Energy.lean 46 declarations
- ExpVector.lean 61 declarations
- ExpectedReindexStates.lean 69 declarations
- Field.lean 71 declarations
- FiniteMaxHamiltonian.lean 47 declarations
- FlipStar.lean 67 declarations
- GenericDegrees.lean 66 declarations
- GlobalDyadicFieldError.lean 44 declarations
- GramBlock.lean 46 declarations
- GramPosSemidef.lean 75 declarations
- HasDerivAtDeviation.lean 30 declarations
- HierarchyNumerator.lean 54 declarations
- HierarchyNumeratorNonneg.lean 27 declarations
- HorizonGrid.lean 56 declarations
- HugeSelectiveBounded.lean 42 declarations
- IdentityErrorFinSumTendsto.lean 42 declarations
- IncrementEqKernel.lean 61 declarations
- InnerRootYCoordinates.lean 53 declarations
- InnovationEulerMemLp.lean 62 declarations
- InsertionApprox.lean 60 declarations
- InsertionFromForward.lean 90 declarations
- IntegrableExpField.lean 67 declarations
- IntegrablePdfMul.lean 65 declarations
- Joint.lean 50 declarations
- Labels.lean 72 declarations
- Law.lean 57 declarations
- LogMean.lean 78 declarations
- LogSeriesTermBound.lean 33 declarations
- LowBlock.lean 58 declarations
- LowVector.lean 59 declarations
- MaskedDisorder.lean 67 declarations
- MeasurableStepParam.lean 56 declarations
- MeasureCoefficientOnSupportGap.lean 30 declarations
- Mix.lean 49 declarations
- MixedMatrixOne.lean 69 declarations
- MixedReplicaIdentity.lean 52 declarations
- Model.lean 68 declarations
- MovingTensorInsertionLimit.lean 45 declarations
- NegativeFlip.lean 39 declarations
- Nnwidth.lean 39 declarations
- OrderPointIntegrable.lean 17 declarations
- OrderedCode.lean 38 declarations
- OrdinaryInverseSpecial.lean 61 declarations
- OverlapDiscountMono.lean 48 declarations
- PacketLabel.lean 47 declarations
- PacketRegular.lean 76 declarations
- ParamGate.lean 67 declarations
- ParisiCanonicalTransport.lean 39 declarations
- ParisiConjugateTransport.lean 23 declarations
- ParisiCoshEntropy.lean 72 declarations
- ParisiEntropyDecomposition.lean 16 declarations
- ParisiFiniteTransport.lean 48 declarations
- ParisiHankelDerivative.lean 46 declarations
- ParisiReflection.lean 30 declarations
- PartitionSite.lean 49 declarations
- PhysicalGate.lean 59 declarations
- RealShiftNormSqLe.lean 37 declarations
- RestrictCode.lean 55 declarations
- RestrictLeft.lean 80 declarations
- ReverseWord.lean 86 declarations
- RotateIJApply.lean 33 declarations
- RotationAccuracy.lean 38 declarations
- ScalarPhase.lean 60 declarations
- ScaledTimeMem.lean 35 declarations
- ScheduleWidthNonneg.lean 44 declarations
- SecondCoefficient.lean 61 declarations
- SelectedBlock.lean 56 declarations
- Shape.lean 61 declarations
- Sine.lean 58 declarations
- Space.lean 120 declarations
- SpinCoeAdd.lean 84 declarations
- SpinFlip.lean 49 declarations
- SpinMatrix.lean 63 declarations
- SpinTrace.lean 42 declarations
- SpinWInv.lean 119 declarations
- SpinWZeroApply.lean 32 declarations
- Splice.lean 35 declarations
- SquareKernel.lean 60 declarations
- SumFinLtNat.lean 59 declarations
- SumLeCode.lean 50 declarations
- TendstoDyadicRound.lean 83 declarations
- Tensor.lean 75 declarations
- TermNormSub.lean 52 declarations
- TerminalThird.lean 16 declarations
- ThermalDeviation.lean 53 declarations
- Time.lean 77 declarations
- TimeCubicTest.lean 42 declarations
- TreeNodeDepth.lean 42 declarations
- UnitaryUp.lean 81 declarations
- UsedVertices.lean 57 declarations
- VarianceProdDecomposition.lean 48 declarations
- WComm.lean 83 declarations
- WeightedGradientField.lean 31 declarations
- WeightedSumPos.lean 46 declarations
- YAdd.lean 49 declarations