OAI/Probability/FreeIsing/Martingales/
301 declarations, 0 contain sorry, 0 declared as axioms; 46 files
Files
- ArtanhMartingaleFormula.lean 18 declarations
- BoundedMartingaleDriftEnergy.lean 5 declarations
- BoundedMartingaleVariation.lean 15 declarations
- BracketIsometry.lean 7 declarations
- CharacteristicStep.lean 8 declarations
- CoefficientApproximation.lean 1 declarations
- ContinuousL2Limit.lean 5 declarations
- ContinuousLimit.lean 2 declarations
- ContinuousMartingaleVariation.lean 2 declarations
- ContinuousMaximal.lean 5 declarations
- ContinuousPosteriorMartingale.lean 2 declarations
- ContinuousSelection.lean 4 declarations
- ContinuousSubsequence.lean 1 declarations
- DominatedMartingaleRightContinuation.lean 5 declarations
- DriftEnergy.lean 11 declarations
- GaussianCriterion.lean 6 declarations
- InnovationMartingale.lean 10 declarations
- IntegerIdentification.lean 5 declarations
- IntegralStability.lean 2 declarations
- L2Closure.lean 3 declarations
- L2MartingaleRightContinuation.lean 2 declarations
- PredictableL2Completion.lean 12 declarations
- PredictableMeshApproximation.lean 22 declarations
- PredictableVersion.lean 5 declarations
- Pushforward.lean 1 declarations
- QuadraticVariation.lean 16 declarations
- RandomEvaluation.lean 6 declarations
- RightContinuation.lean 5 declarations
- SpatialCompensator.lean 1 declarations
- SpatialLimit.lean 7 declarations
- SpatialPredictableL2.lean 4 declarations
- SpatialRandomEvaluation.lean 3 declarations
- SquareMaximal.lean 4 declarations
- StoppedDiscrepancyEnergy.lean 4 declarations
- StoppedEnergyRiemann.lean 5 declarations
- StoppedIdentityExhaustion.lean 2 declarations
- StoppedMartingaleL2.lean 5 declarations
- StoppedProcessExhaustion.lean 2 declarations
- StoppedProcessTransport.lean 10 declarations
- StoppedRowNormalization.lean 2 declarations
- StoppedSpatialAssociativity.lean 1 declarations
- StoppedTimePrimitive.lean 8 declarations
- StrongMaximal.lean 37 declarations
- TaylorRemainder.lean 7 declarations
- TransformL2.lean 9 declarations
- UniformIntegral.lean 4 declarations