OAI/InformationTheory/Entanglement/
1158 declarations, 0 contain sorry, 0 declared as axioms; 151 files
Files
- ActualDefaults.lean 5 declarations
- AdaptivePublic.lean 4 declarations
- ArbitraryPurificationConsumer.lean 1 declarations
- BinomialDimension.lean 4 declarations
- BooleanSpan.lean 10 declarations
- CPBlocks.lean 7 declarations
- CQVariation.lean 8 declarations
- CausalIndependence.lean 12 declarations
- CausalPublic.lean 8 declarations
- CausalRealization.lean 4 declarations
- CausalSampler.lean 18 declarations
- ChoiTransfer.lean 6 declarations
- Coherence.lean 2 declarations
- CombinatorialAssembly.lean 10 declarations
- CombinatorialLocal.lean 11 declarations
- CombinatorialMain.lean 28 declarations
- CombinatorialNumbers.lean 19 declarations
- CombinatorialOrder.lean 36 declarations
- CombinatorialQuestions.lean 17 declarations
- ConditionalUpdate.lean 13 declarations
- ConditionedLaw.lean 8 declarations
- CorrelationBound.lean 3 declarations
- CyclicCharpoly.lean 4 declarations
- DefaultNull.lean 8 declarations
- DensityChange.lean 10 declarations
- DensityGap.lean 13 declarations
- DensityPositivity.lean 8 declarations
- EffectNormalization.lean 4 declarations
- EightSubsetCardinality.lean 4 declarations
- EveBlocks.lean 7 declarations
- FactorizedLawGap.lean 10 declarations
- FiberBound.lean 9 declarations
- FidelityTools.lean 12 declarations
- FiniteInputInstrument.lean 11 declarations
- FiniteLawRecovery.lean 2 declarations
- FiniteRecovery.lean 9 declarations
- FirstBitLaw.lean 5 declarations
- FullQuantumConsumer.lean 2 declarations
- FunctionCardinality.lean 1 declarations
- HermitianBanach.lean 22 declarations
- HermitianInstrument.lean 15 declarations
- HilbertCanonicalRecovery.lean 2 declarations
- HilbertChannel.lean 7 declarations
- HilbertChannelMeasure.lean 12 declarations
- HilbertCoarsegrain.lean 8 declarations
- HilbertConditioning.lean 5 declarations
- HilbertENorm.lean 5 declarations
- HilbertEmbedding.lean 6 declarations
- HilbertEmbeddingOrder.lean 4 declarations
- HilbertLawAlgebra.lean 9 declarations
- HilbertLawDistance.lean 7 declarations
- HilbertLawFinite.lean 6 declarations
- HilbertLawMetric.lean 10 declarations
- HilbertLawRecovery.lean 2 declarations
- HilbertLawScale.lean 4 declarations
- HilbertMeasure.lean 10 declarations
- HilbertMeasureEmbedding.lean 7 declarations
- HilbertRecordMap.lean 7 declarations
- HilbertRecovery.lean 10 declarations
- HilbertTensor.lean 14 declarations
- HilbertTrace.lean 14 declarations
- HilbertTraceDifference.lean 3 declarations
- HilbertTraceIdeal.lean 7 declarations
- HilbertVectorMeasure.lean 12 declarations
- IndependentTapes.lean 12 declarations
- InformationalComplete.lean 12 declarations
- InstrumentContraction.lean 3 declarations
- InstrumentCovariance.lean 4 declarations
- InstrumentLaw.lean 9 declarations
- InstrumentMeasure.lean 6 declarations
- KernelSampling.lean 3 declarations
- KeyRates.lean 2 declarations
- LinearPolynomialCertificate.lean 5 declarations
- LocalMemoryKernels.lean 7 declarations
- LocalStateVisibility.lean 1 declarations
- Main.lean 150 imports, no declarations
- MainStateAlgebra.lean 20 declarations
- MatrixDensityChange.lean 5 declarations
- MatrixFamilyDensity.lean 13 declarations
- MatrixMeasurability.lean 3 declarations
- MatrixMeasure.lean 9 declarations
- MatrixMeasureChannel.lean 15 declarations
- MatrixPolar.lean 4 declarations
- MatrixTraceMeasure.lean 15 declarations
- MultiTensor.lean 13 declarations
- NormalizeRepresentation.lean 4 declarations
- NormalizedProbe.lean 10 declarations
- NormalizedPurificationConsumer.lean 3 declarations
- OperationalNorm.lean 3 declarations
- ParityData.lean 19 declarations
- ParityObstruction.lean 14 declarations
- PhysicalAdaptiveStep.lean 2 declarations
- PhysicalChronology.lean 2 declarations
- PhysicalConditionalUpdate.lean 3 declarations
- PhysicalExecutionStep.lean 4 declarations
- PhysicalHistoryRealization.lean 1 declarations
- PhysicalProductStep.lean 10 declarations
- PhysicalPublicPrefix.lean 1 declarations
- PhysicalRawPrefix.lean 1 declarations
- PhysicalRightAdaptive.lean 2 declarations
- PhysicalRightRawPrefix.lean 1 declarations
- PhysicalRightStep.lean 6 declarations
- PhysicalVersion.lean 1 declarations
- PolynomialGcdDegree.lean 4 declarations
- PositiveBlock.lean 9 declarations
- PowersStormer.lean 4 declarations
- ProbeDensity.lean 2 declarations
- ProbeFactorization.lean 4 declarations
- ProbeMatrices.lean 6 declarations
- ProbePOVM.lean 10 declarations
- ProbeRescaling.lean 5 declarations
- ProductInstrumentStep.lean 4 declarations
- ProjectionData.lean 23 declarations
- ProjectionMain.lean 2 declarations
- ProjectionReal.lean 14 declarations
- ProjectionRealMain.lean 7 declarations
- ProjectionReindex.lean 6 declarations
- ProjectionSquare.lean 10 declarations
- ProjectionStats.lean 13 declarations
- PublicSampler.lean 1 declarations
- PurificationExpansion.lean 1 declarations
- PurificationSupport.lean 2 declarations
- QuantumStepKernel.lean 3 declarations
- ReferenceFilter.lean 9 declarations
- RestrictedIntersections.lean 6 declarations
- ScalarGap.lean 6 declarations
- SecretDefinitions.lean 2 declarations
- SequentialSampling.lean 16 declarations
- SparseSeparable.lean 10 declarations
- SpectralCut.lean 4 declarations
- SpectralWeights.lean 10 declarations
- SplittingEmbedding.lean 3 declarations
- TensorClosure.lean 18 declarations
- TensorPowers.lean 18 declarations
- TensorTools.lean 10 declarations
- TestedQuantumConsumer.lean 2 declarations
- TraceClassModel.lean 12 declarations
- TraceContractivity.lean 3 declarations
- TraceInstrument.lean 11 declarations
- TraceMatrixSpace.lean 19 declarations
- TraceNorm.lean 14 declarations
- TraceStateBounds.lean 3 declarations
- TraceTensor.lean 16 declarations
- TranscriptClassical.lean 3 declarations
- TranscriptLimit.lean 1 declarations
- WeakIntegralForm.lean 5 declarations
- WeakLawTrace.lean 2 declarations
- WeakProductPrefix.lean 3 declarations
- WeakStateSupport.lean 8 declarations
- WeakStateUnique.lean 3 declarations
- WeakTensorMeasurable.lean 2 declarations