OAI/Probability/SKGap/Localization/
3264 declarations, 0 contain sorry, 0 declared as axioms; 243 files
Files
- AffineBilinear.lean 11 declarations
- AffineUpper.lean 4 declarations
- Append.lean 22 declarations
- AttractionBasinIUnion.lean 9 declarations
- Bilinear.lean 15 declarations
- Bilinear2.lean 9 declarations
- BilinearCoefficient.lean 17 declarations
- BilinearUnion.lean 17 declarations
- BlockDegree.lean 23 declarations
- BoundedIntervalFubini.lean 2 declarations
- BoxChaining.lean 3 declarations
- BufferedComparisonBound.lean 2 declarations
- BufferedFlip.lean 7 declarations
- BufferedSelectionDiagnostics.lean 6 declarations
- Centered.lean 14 declarations
- ChainingCore.lean 7 declarations
- Character.lean 50 declarations
- ClosedMarked.lean 60 declarations
- ClosedMarkedControl.lean 21 declarations
- ClosedPrediction.lean 27 declarations
- CoefficientFlip.lean 6 declarations
- CoefficientInputBridge.lean 2 declarations
- CoefficientRow.lean 16 declarations
- CompactTube.lean 12 declarations
- ComponentRefresh.lean 18 declarations
- CondSubConst.lean 17 declarations
- ConditionalEmpiricalLaw.lean 5 declarations
- ConditionalHessianLaw.lean 11 declarations
- ConditionalIntegralRate.lean 7 declarations
- ConditionalMiddleSize.lean 4 declarations
- ConditionalModelAlgebra.lean 20 declarations
- ConditionalRankAlgebra.lean 12 declarations
- ConditionalTolerance.lean 11 declarations
- ConditionalWeight.lean 7 declarations
- ConditionalWellDefined.lean 3 declarations
- Conjugation.lean 13 declarations
- ConstantRecipe.lean 18 declarations
- CoordinateDeriv.lean 12 declarations
- CoordinateLipschitz.lean 25 declarations
- CubeApprox.lean 6 declarations
- CubeWeight.lean 18 declarations
- CurieWeiss.lean 27 declarations
- CyclicPrediction.lean 6 declarations
- DerivNonnegRightMin.lean 6 declarations
- DiagonalHessianJoined.lean 16 declarations
- DiagonalSqrt.lean 8 declarations
- DiagonalSum.lean 11 declarations
- DiagonalTMemLp.lean 5 declarations
- DimensionDecay.lean 16 declarations
- DimensionDecayPos.lean 9 declarations
- DisorderRecipeEvent.lean 7 declarations
- DivergenceIntegrand.lean 51 declarations
- DoublePlantedLawTransfer.lean 3 declarations
- DriftSquare.lean 9 declarations
- EmpiricalConditionalData.lean 7 declarations
- EmpiricalGramBound.lean 5 declarations
- EmpiricalLaw.lean 6 declarations
- EntryLM.lean 19 declarations
- Envelope.lean 12 declarations
- EqualityCurve.lean 20 declarations
- Error.lean 23 declarations
- ExpAbsSum.lean 4 declarations
- ExpDrift.lean 13 declarations
- ExpDuhamel.lean 22 declarations
- ExpSum.lean 38 declarations
- ExpectedCutoff.lean 8 declarations
- FiniteMax.lean 23 declarations
- FiniteRankPositive.lean 26 declarations
- FiniteRecipeControl.lean 7 declarations
- FiniteStartedControlGeneral.lean 7 declarations
- FixedTimeQuenched.lean 12 declarations
- FockSeries.lean 34 declarations
- FrobeniusSq.lean 6 declarations
- GeneralTemplateRegularity.lean 10 declarations
- GeneratorNonposMax.lean 4 declarations
- GramColumnBounds.lean 4 declarations
- GramRobust.lean 2 declarations
- GramUniformRobust.lean 8 declarations
- GraphPrediction.lean 20 declarations
- GridSteps.lean 19 declarations
- IntegrableLinearCombinationSq.lean 13 declarations
- IntegrableMulBounded.lean 14 declarations
- IntegrableResidualRecipeSq.lean 2 declarations
- IntegralAbsSet.lean 4 declarations
- IntegralProductDeviation.lean 2 declarations
- Invert.lean 26 declarations
- JumpBilinear.lean 22 declarations
- JumpEnergy.lean 21 declarations
- JumpWeight.lean 24 declarations
- KernelDensity.lean 3 declarations
- Letter.lean 44 declarations
- LinSub.lean 21 declarations
- LinearObservable.lean 16 declarations
- LiteralConstruction.lean 7 declarations
- LiteralInitialRecipe.lean 12 declarations
- LiteralInitialSystem.lean 21 declarations
- LiteralLocalInput.lean 3 declarations
- LiteralLocalWeak.lean 3 declarations
- LiteralMargin.lean 5 declarations
- LiteralPartial.lean 2 declarations
- LiteralRegularity.lean 7 declarations
- LiteralSeriesLiftAppend.lean 19 declarations
- LiteralSystemBridge.lean 4 declarations
- LiteralValues.lean 3 declarations
- LiteralWeak.lean 5 declarations
- LocalCoefficient.lean 12 declarations
- LocalExtraction.lean 5 declarations
- LocalFixedRecipe.lean 2 declarations
- LocalRecipeClass.lean 11 declarations
- LocalResidualInduction.lean 6 declarations
- LocalStartedDiagonal.lean 10 declarations
- LocalUniformWeak.lean 17 declarations
- LocalVolumeChange.lean 11 declarations
- LocalVolumeEnergy.lean 14 declarations
- LocalVolumeFull.lean 3 declarations
- LocalWeakBase.lean 6 declarations
- LocalWhitening.lean 9 declarations
- LogPartitionDeviationProbability.lean 2 declarations
- LogQuadratic.lean 23 declarations
- Magnetization.lean 35 declarations
- Map.lean 25 declarations
- MarkedDiagnostic.lean 16 declarations
- MarkedErrorRate.lean 4 declarations
- MarkedProductIBP.lean 4 declarations
- ModelLocalization.lean 1 declarations
- NoiseSplit.lean 20 declarations
- Operation.lean 23 declarations
- OperatorQuenched.lean 6 declarations
- OriginalEventRegeneration.lean 8 declarations
- PartitionChangeMeasure.lean 2 declarations
- PartitionLogLipschitz.lean 3 declarations
- PhiAlgebra.lean 19 declarations
- PhiBounds.lean 21 declarations
- PhiCoefficient.lean 7 declarations
- PhiFrechet.lean 35 declarations
- PhiHessianBridge.lean 5 declarations
- PhiRatio.lean 16 declarations
- PhiRegularity.lean 14 declarations
- PhiResponse.lean 9 declarations
- PlantedFixedTime.lean 10 declarations
- PlantedMarginalLaw.lean 9 declarations
- PlantedTilt.lean 6 declarations
- PoissonBinomial.lean 5 declarations
- PoissonBinomialProbability.lean 26 declarations
- PoissonWeight.lean 21 declarations
- PositiveRamp.lean 16 declarations
- Prediction.lean 3 declarations
- PreparationGrowth.lean 26 declarations
- PrimaryDifferentiation.lean 13 declarations
- PrimaryFiniteControl.lean 1 declarations
- PrimaryLocalInput.lean 14 declarations
- PrimaryPrediction.lean 73 declarations
- PrimaryQuenched.lean 6 declarations
- ProdEventSectionLaw.lean 14 declarations
- ProjectedMarkedIBP.lean 2 declarations
- ProjectedReal.lean 12 declarations
- Quadratic.lean 13 declarations
- QuadraticCoeff.lean 11 declarations
- QuenchedHelpers.lean 8 declarations
- QueryColumn.lean 26 declarations
- QueryResidual.lean 18 declarations
- RankCovariance.lean 14 declarations
- RareCoordinate.lean 7 declarations
- RealParameterIncrement.lean 12 declarations
- RealPart.lean 19 declarations
- RealQuadratic.lean 6 declarations
- RecipeArgumentPullback.lean 16 declarations
- RecipeBound.lean 6 declarations
- RecipeCoefficientClosure.lean 7 declarations
- RecipeError.lean 8 declarations
- RecipeGraph.lean 13 declarations
- RecipeIncrement.lean 9 declarations
- RecipeMarked.lean 18 declarations
- RecipePrimaryMass.lean 4 declarations
- Reference.lean 54 declarations
- RefreshGenerator.lean 45 declarations
- RegeneratedAnswer.lean 9 declarations
- ResidualAdmissibility.lean 12 declarations
- ResidualInduction.lean 17 declarations
- ResidualMultiplier.lean 23 declarations
- ResidualRecipe.lean 19 declarations
- ResidualRecipe2.lean 20 declarations
- ResidualSelection.lean 8 declarations
- SampledFlatCLM.lean 17 declarations
- SandShift.lean 17 declarations
- SandShiftSpecial.lean 5 declarations
- ScalarClosedIsolation.lean 5 declarations
- ScalarConsistency.lean 10 declarations
- ScalarEigenfunction.lean 25 declarations
- ScalarEmpirical.lean 15 declarations
- ScalarFixedPointJoined.lean 46 declarations
- ScalarParametersJoined.lean 43 declarations
- ScalarRelativeIsolation.lean 4 declarations
- ScalarSlowConeStep.lean 5 declarations
- ScalarSmallNoiseTests.lean 9 declarations
- ScalarVariance.lean 24 declarations
- SelectionDeficit.lean 4 declarations
- SelectionPartition.lean 9 declarations
- SemicircleDensity.lean 18 declarations
- SemigroupAbs.lean 7 declarations
- SeparateCut.lean 14 declarations
- SeparatedCard.lean 3 declarations
- SmallOverlap.lean 4 declarations
- SmoothSelection.lean 23 declarations
- SparseCubeNet.lean 10 declarations
- SparseQuadratic.lean 2 declarations
- SparseShrink.lean 3 declarations
- StandardArrayLaw.lean 37 declarations
- StartedFixed.lean 9 declarations
- StartedGraph.lean 14 declarations
- StartedMarked.lean 7 declarations
- StartedPrefix.lean 7 declarations
- StartedPrimary.lean 9 declarations
- StartedRecipe.lean 13 declarations
- StartedResidualStep.lean 11 declarations
- StartedSmall.lean 11 declarations
- StationaryInner.lean 21 declarations
- StepMass.lean 15 declarations
- SumPoissonMass.lean 6 declarations
- SusceptibilityMiddle.lean 7 declarations
- SusceptibilityTest.lean 3 declarations
- SymmetricElementaryComm.lean 3 declarations
- TAPGauge.lean 12 declarations
- TAPScalarTaylor.lean 7 declarations
- TAPVectorTaylor.lean 13 declarations
- TanhContDiff.lean 8 declarations
- TanhCubic.lean 2 declarations
- TapPotential.lean 38 declarations
- TargetAttempt.lean 13 declarations
- Taylor.lean 2 declarations
- TemplateChaining.lean 3 declarations
- TemplatePatterns.lean 3 declarations
- ThresholdChoice.lean 15 declarations
- TruncationGoodSet.lean 7 declarations
- UniformRecipeClass.lean 14 declarations
- UniformResidual.lean 19 declarations
- UniformSquareInduction.lean 5 declarations
- UniformStarted.lean 4 declarations
- UnitBall.lean 22 declarations
- UpperClockTendstoTop.lean 4 declarations
- UpperCoefficient.lean 32 declarations
- Vectorize.lean 39 declarations
- WeakResidual.lean 19 declarations