OAI/Analysis/CircleDomains/Probability/
893 declarations, 0 contain sorry, 0 declared as axioms; 230 files
Files
- AffinePhysicalOccupation.lean 2 declarations
- AffinePhysicalTimeMeasure.lean 3 declarations
- AffineResidualNull.lean 2 declarations
- AffineTimeMeasure.lean 2 declarations
- AnalyticFiniteMeasurability.lean 3 declarations
- ArcBoundaryMeasure.lean 4 declarations
- ArcImageMeasures.lean 2 declarations
- ArcNullImage.lean 2 declarations
- AtomicVisitMeasure.lean 5 declarations
- BandMeasure.lean 6 declarations
- BarrierCodeLaw.lean 3 declarations
- BorelDensityBudget.lean 2 declarations
- BorelFamilyHitFusion.lean 1 declarations
- BorelFiberCounts.lean 7 declarations
- BorelImageCompactModulus.lean 1 declarations
- CenteredArcLaw.lean 6 declarations
- CenteredSubtypeLaw.lean 1 declarations
- CenteredTerminalLaw.lean 11 declarations
- CircleNullImage.lean 2 declarations
- CircleSupportedLaw.lean 3 declarations
- ClippedArcOccupation.lean 2 declarations
- ClosedFusionScheme.lean 6 declarations
- ClosedProbabilitySupport.lean 2 declarations
- ClosedSubsetHitFusion.lean 1 declarations
- CodeHitMeasures.lean 11 declarations
- CodeLawAbsoluteContinuity.lean 3 declarations
- CodeLawCandidateBounds.lean 3 declarations
- CodeLawCandidateConsequences.lean 3 declarations
- CodeLawCandidates.lean 5 declarations
- CodeLawMeasures.lean 11 declarations
- CodeLawMixtures.lean 6 declarations
- CodeLawPhysicalOccupation.lean 2 declarations
- CodeLocalBandTagNull.lean 2 declarations
- CodePairOccupation.lean 3 declarations
- CodePathLaws.lean 6 declarations
- CodeRealBandTagNull.lean 2 declarations
- CollarAlternationProbability.lean 1 declarations
- CollarTimeMeasures.lean 3 declarations
- CommonPointNullSet.lean 2 declarations
- CompactArcLaw.lean 5 declarations
- CompactFiniteMeasureBorel.lean 4 declarations
- CompactFiniteMeasureMeasurability.lean 3 declarations
- CompactLawSplit.lean 4 declarations
- CompactMeasureBarycenter.lean 6 declarations
- CompactMeasureContinuity.lean 1 declarations
- CompactMeasureDensity.lean 3 declarations
- CompactMeasureDuality.lean 1 declarations
- CompactMeasureMajorantCost.lean 11 declarations
- CompactMeasureMajorants.lean 4 declarations
- CompactMeasureSeparation.lean 3 declarations
- CompactPhysicalArcLaw.lean 1 declarations
- CompactPlanTestDensity.lean 1 declarations
- CompactProbabilityBorel.lean 2 declarations
- ConcatenatedResidualNull.lean 2 declarations
- ConfigurationMeasures.lean 7 declarations
- ConstrainedCodeLaws.lean 6 declarations
- ContinuousLawMeasurable.lean 1 declarations
- ContinuousMeasureModulus.lean 2 declarations
- CountableCodedCollarLaws.lean 1 declarations
- CountableCollarLaws.lean 1 declarations
- CountableDiffuseCodeLaws.lean 1 declarations
- CountableExtractionFusion.lean 1 declarations
- CountableLawExtraction.lean 1 declarations
- CountableLawRestriction.lean 2 declarations
- CountableQuotientCodeLaws.lean 1 declarations
- CountableRecursiveLaws.lean 1 declarations
- CountableSquareLawBounds.lean 3 declarations
- CountableVisitNorm.lean 6 declarations
- DelayedTupleMeasure.lean 4 declarations
- DensityBudgetMixture.lean 2 declarations
- DensityMassBound.lean 4 declarations
- DiskStartLaw.lean 4 declarations
- DomainPhysicalOccupation.lean 4 declarations
- DominatedDensity.lean 2 declarations
- DyadicMeasurePartition.lean 3 declarations
- DyadicPhysicalOccupation.lean 9 declarations
- ExactBandMeasure.lean 3 declarations
- ExitTimeMeasurability.lean 7 declarations
- FatouSelection.lean 2 declarations
- FiniteChoiceLaw.lean 3 declarations
- FiniteLevelNullImage.lean 1 declarations
- FiniteMeasureCoordinates.lean 7 declarations
- FiniteMeasureTightControl.lean 1 declarations
- FiniteTupleLevelLaws.lean 2 declarations
- FullLevelNullImage.lean 1 declarations
- FusionKernel.lean 1 declarations
- FusionSmallSets.lean 9 declarations
- FusionTrajectory.lean 10 declarations
- GDeltaPolish.lean 1 declarations
- GatePenaltyDensity.lean 1 declarations
- GatedRecursiveLaw.lean 1 declarations
- GeometricIndexMeasurable.lean 2 declarations
- GlobalSphericalDensity.lean 4 declarations
- GraphNullFibers.lean 1 declarations
- HausdorffZeroCounting.lean 2 declarations
- HeightHorizontalNullPair.lean 1 declarations
- HitFusion.lean 7 declarations
- HitFusionCaps.lean 6 declarations
- HitFusionLaw.lean 12 declarations
- HitFusionTree.lean 13 declarations
- HorizontalNullPair.lean 7 declarations
- IncreasingMeasureLimit.lean 6 declarations
- IntervalCoverMeasure.lean 2 declarations
- IntervalPaymentNullImage.lean 2 declarations
- LastEntryCircleLaw.lean 3 declarations
- LastEntryLaw.lean 4 declarations
- LawLocalBandTagNull.lean 1 declarations
- LawRealBandTagNull.lean 1 declarations
- LengthContentNull.lean 2 declarations
- LevelLawQuantifiers.lean 1 declarations
- LevelPaymentMeasure.lean 3 declarations
- LocalHorizontalNullPair.lean 1 declarations
- LocalMassVanishing.lean 1 declarations
- LocalNullImage.lean 1 declarations
- LocalPartialMeasurability.lean 1 declarations
- LocalizedDensityNorm.lean 2 declarations
- LocalizedSquareMass.lean 2 declarations
- MarkedFusionKernel.lean 1 declarations
- MarkedFusionSmallSets.lean 8 declarations
- MarkedHitFusion.lean 7 declarations
- MarkedHitFusionCaps.lean 6 declarations
- MarkedHitFusionLaw.lean 12 declarations
- MarkedHitFusionTree.lean 13 declarations
- MarkedHitLaws.lean 9 declarations
- MeanVisitDensity.lean 6 declarations
- MeasurableArcIndex.lean 14 declarations
- MeasurableBaireBranch.lean 1 declarations
- MeasurableLinearInverse.lean 1 declarations
- MeasurablePieceInverse.lean 4 declarations
- MeasurableRangeSection.lean 1 declarations
- MeasurableRaySides.lean 3 declarations
- MeasurableTerminalArcs.lean 2 declarations
- MeasureFamilyBoundedSequence.lean 1 declarations
- MeasureFamilyCompactLocalization.lean 1 declarations
- MeasureFamilyDominatedLimit.lean 3 declarations
- MeasureFamilyExceptional.lean 1 declarations
- MeasureFamilyIncreasing.lean 2 declarations
- MeasureFamilyModulusBasic.lean 7 declarations
- MeasureFamilyNullMetric.lean 1 declarations
- MeasureFamilyNullRemoval.lean 2 declarations
- MeasureFamilyNullUnions.lean 1 declarations
- MeasureFamilyPositivePiece.lean 2 declarations
- MeasureFamilySignedLimit.lean 1 declarations
- MeasureFamilySubadditivity.lean 2 declarations
- MeasureImageDualityProof.lean 1 declarations
- MeasureQuadraticSum.lean 1 declarations
- MeetingFatou.lean 1 declarations
- MomentLawBounds.lean 4 declarations
- MonotoneDyadicMass.lean 2 declarations
- NullImage.lean 1 declarations
- NullLevelTuples.lean 8 declarations
- NullPairFromLevels.lean 2 declarations
- OccupationNeighborhood.lean 1 declarations
- OccupationProduct.lean 3 declarations
- OpenLineImageMeasure.lean 1 declarations
- ParametricNullTuples.lean 4 declarations
- PathCostMeasure.lean 24 declarations
- PathHitLaws.lean 11 declarations
- PathImageOccupation.lean 5 declarations
- PathIntersectionMeasure.lean 10 declarations
- PathLawMixtures.lean 14 declarations
- PathLengthMeasure.lean 9 declarations
- PathOccupation.lean 11 declarations
- PathPortionMeasure.lean 7 declarations
- PhysicalImageOccupation.lean 9 declarations
- PhysicalLastEntryLaw.lean 1 declarations
- PhysicalLawRebasing.lean 7 declarations
- PhysicalLineFubini.lean 3 declarations
- PhysicalOccupationAdd.lean 2 declarations
- PhysicalOccupationCode.lean 8 declarations
- PhysicalOccupationCost.lean 4 declarations
- PhysicalOccupationPushforward.lean 7 declarations
- PhysicalPieceTimeMeasure.lean 1 declarations
- PhysicalSliceOccupation.lean 3 declarations
- PointHitOccupation.lean 2 declarations
- PointHitPairOccupation.lean 2 declarations
- PolishProbabilityProof.lean 1 declarations
- PositiveBarrierLaw.lean 1 declarations
- PositiveCodeLawFusion.lean 1 declarations
- PositiveMassCompactLocalization.lean 1 declarations
- PotentialMeasurability.lean 1 declarations
- PotentialRectangleMeasurability.lean 1 declarations
- PrincipalDensityStability.lean 2 declarations
- PriorBarrierCodeLaw.lean 2 declarations
- PriorLawPresentation.lean 2 declarations
- PriorPositiveBarrierLaw.lean 1 declarations
- ProbabilityImageLifting.lean 2 declarations
- ProbabilityMeasureEmbedding.lean 4 declarations
- ProbabilityMixtureMap.lean 2 declarations
- ProbabilitySquareBounds.lean 3 declarations
- ProbabilityTopologicalEmbedding.lean 1 declarations
- PublishedMeasureDuality.lean 4 declarations
- PublishedProbabilityTopology.lean 2 declarations
- RandomShifts.lean 6 declarations
- RayFamilyMeasurable.lean 4 declarations
- RectangleMeasurability.lean 1 declarations
- RectifiableOccupationCode.lean 6 declarations
- RecursiveCodeLaw.lean 46 declarations
- RecursiveLawConstruction.lean 4 declarations
- RecursiveLawContacts.lean 1 declarations
- RecursiveLawLevelEstimates.lean 1 declarations
- RecursiveLawSelection.lean 1 declarations
- ResidualTailNull.lean 5 declarations
- ReversedPhysicalOccupation.lean 6 declarations
- ScalarPairNull.lean 3 declarations
- SelectableMeanLaw.lean 1 declarations
- SimpleArcDomainDensity.lean 2 declarations
- SimpleArcMeasurability.lean 5 declarations
- SimpleArcOccupation.lean 5 declarations
- SimplePhysicalArcOccupation.lean 3 declarations
- SliceDensityNorm.lean 3 declarations
- SliceMeasurability.lean 2 declarations
- SlotLawMeasures.lean 7 declarations
- SlotPairNull.lean 4 declarations
- SparseTupleMeasure.lean 5 declarations
- SphericalDensityNorm.lean 1 declarations
- SphericalSliceDensity.lean 6 declarations
- StandardBorelEmbedding.lean 1 declarations
- StandardBorelProbabilityProof.lean 1 declarations
- StartingLawBoundaryGate.lean 3 declarations
- SummableErrorExtraction.lean 1 declarations
- SummableRecursiveBudget.lean 4 declarations
- SummableTestLimits.lean 2 declarations
- SupportedProbability.lean 3 declarations
- SupportedProbabilityGDelta.lean 2 declarations
- TagPaymentMeasure.lean 8 declarations
- TagTupleMeasure.lean 22 declarations
- TerminalArcLaw.lean 5 declarations
- TerminalPathMeasurability.lean 3 declarations
- TupleProductNull.lean 1 declarations