OAI/Analysis/Pureness/States/
411 declarations, 0 contain sorry, 0 declared as axioms; 68 files
Files
- CauchyQuotientAdditivity.lean 3 declarations
- FiniteFamilyAWPositive.lean 11 declarations
- FiniteFamilyAmplification.lean 9 declarations
- FiniteFamilyBaseCarrier.lean 11 declarations
- FiniteFamilyBlockValues.lean 6 declarations
- FiniteFamilyBounds.lean 5 declarations
- FiniteFamilyCarrier.lean 8 declarations
- FiniteFamilyCompletion.lean 16 declarations
- FiniteFamilyExtremalCompletion.lean 3 declarations
- FiniteFamilyExtremalRestriction.lean 1 declarations
- FiniteFamilyFreeGroup.lean 9 declarations
- FiniteFamilyMatrixCompletion.lean 11 declarations
- FiniteFamilyMatrixRank.lean 2 declarations
- FiniteFamilyMatrixTrace.lean 3 declarations
- FiniteFamilyMetric.lean 6 declarations
- FiniteFamilyNormalizedMatrices.lean 7 declarations
- FiniteFamilyNuclearSpatial.lean 9 declarations
- FiniteFamilyNuclearTrace.lean 6 declarations
- FiniteFamilyPullback.lean 10 declarations
- FiniteFamilyRegularized.lean 7 declarations
- FiniteFamilyScalarRank.lean 4 declarations
- FiniteFamilyScalarUltraproduct.lean 9 declarations
- FiniteFamilyScalarValue.lean 2 declarations
- FiniteFamilySpatialExtension.lean 7 declarations
- FiniteFamilyTraceReduction.lean 8 declarations
- FiniteFamilyUltraproduct.lean 9 declarations
- FiniteQuasitraceCStarValue.lean 6 declarations
- FiniteQuasitraceCauchyValue.lean 7 declarations
- FiniteRegularizationAddition.lean 12 declarations
- FiniteRegularizationContinuity.lean 6 declarations
- FiniteRegularizationProjections.lean 4 declarations
- FiniteStateComparison.lean 4 declarations
- FiniteStateRegularization.lean 4 declarations
- NormalizedMatrixStateDiagonal.lean 8 declarations
- NormalizedMatrixStateScalar.lean 5 declarations
- NormalizedMatrixStateUltraRank.lean 4 declarations
- NormalizedMatrixStateUltraproduct.lean 12 declarations
- NormalizedPositiveState.lean 4 declarations
- NormalizedStateAWStar.lean 2 declarations
- NormalizedStateQuotientQuasitrace.lean 5 declarations
- NormalizedStateQuotientTwoQuasitrace.lean 5 declarations
- OriginalFreeGroupQuasitrace.lean 7 declarations
- OriginalScalarNuclearQuasitrace.lean 7 declarations
- OriginalScalarNuclearTensor.lean 9 declarations
- QuotientAWStar.lean 3 declarations
- QuotientAnnihilatorMaximum.lean 1 declarations
- QuotientCentralValueDensity.lean 1 declarations
- QuotientCommutingAdditivity.lean 1 declarations
- QuotientFactorTrace.lean 2 declarations
- QuotientGenuineQuasitrace.lean 5 declarations
- QuotientMatrixCornerLift.lean 7 declarations
- RegularizedStateCStarValue.lean 6 declarations
- RegularizedStateCauchyEmbedding.lean 6 declarations
- RegularizedStateExtendedAW.lean 8 declarations
- RegularizedStateFreeGroupExactness.lean 4 declarations
- RegularizedStateQuasitrace.lean 5 declarations
- RegularizedStateQuotientTrace.lean 3 declarations
- RegularizedStateSpatialFaithful.lean 3 declarations
- RegularizedStateSpatialTransport.lean 6 declarations
- RegularizedStateTraceIdentification.lean 3 declarations
- ScalarCorner.lean 2 declarations
- ScalarMatrixEmbedding.lean 5 declarations
- ScalarMatrixQuasitrace.lean 4 declarations
- ScalarMatrixTrace.lean 12 declarations
- ScalarMatrixUltraEmbedding.lean 8 declarations
- ScalarTracialUltraproductTrace.lean 16 declarations
- ScalarTracialUltraproductValue.lean 2 declarations
- ScalarUltraproductGNS.lean 5 declarations