OAI/Analysis/Pureness/Quasitrace/
505 declarations, 0 contain sorry, 0 declared as axioms; 83 files
Files
- AdditiveQuasitraceTrace.lean 6 declarations
- CentralQuasitraceCompression.lean 5 declarations
- ComplexQuasitraceBounds.lean 8 declarations
- ComplexQuasitracePositive.lean 4 declarations
- ComplexQuasitracePullback.lean 3 declarations
- NormalizedQuasitraceCarrier.lean 10 declarations
- PositiveQuasitrace.lean 5 declarations
- PositiveQuasitraceScaling.lean 7 declarations
- QuasitraceBaseExtremal.lean 11 declarations
- QuasitraceBoundedCompletion.lean 17 declarations
- QuasitraceCauchy.lean 15 declarations
- QuasitraceCauchyAlgebra.lean 3 declarations
- QuasitraceComplex.lean 10 declarations
- QuasitraceComplexLimits.lean 3 declarations
- QuasitraceComplexNormContinuity.lean 3 declarations
- QuasitraceConstantEmbedding.lean 3 declarations
- QuasitraceContinuity.lean 3 declarations
- QuasitraceDistance.lean 13 declarations
- QuasitraceExtremalReduction.lean 6 declarations
- QuasitraceFamily.lean 7 declarations
- QuasitraceFilteredNull.lean 15 declarations
- QuasitraceFilteredQuotient.lean 10 declarations
- QuasitraceFunctionCarrier.lean 7 declarations
- QuasitraceMatrixDiagonal.lean 5 declarations
- QuasitraceMetricContinuity.lean 6 declarations
- QuasitraceMetricFromSqrt.lean 2 declarations
- QuasitraceMetricSize.lean 11 declarations
- QuasitraceNaturality.lean 5 declarations
- QuasitraceNonUnitalRestriction.lean 4 declarations
- QuasitraceNormBounds.lean 7 declarations
- QuasitraceNormalization.lean 6 declarations
- QuasitraceNullApproximateUnit.lean 11 declarations
- QuasitraceNullIdeal.lean 10 declarations
- QuasitracePartsCauchy.lean 4 declarations
- QuasitracePositiveMetricContinuity.lean 9 declarations
- QuasitraceProportionalFunctor.lean 8 declarations
- QuasitraceProportionalMetric.lean 7 declarations
- QuasitracePullback.lean 2 declarations
- QuasitraceQuadraticOrder.lean 3 declarations
- QuasitraceQuotientAnnihilator.lean 3 declarations
- QuasitraceQuotientBallComplete.lean 3 declarations
- QuasitraceQuotientBoundedLimits.lean 5 declarations
- QuasitraceQuotientCFC.lean 5 declarations
- QuasitraceQuotientCStar.lean 4 declarations
- QuasitraceQuotientDensity.lean 2 declarations
- QuasitraceQuotientFaithfulness.lean 2 declarations
- QuasitraceQuotientFinite.lean 1 declarations
- QuasitraceQuotientFiniteSpectrumValue.lean 3 declarations
- QuasitraceQuotientFunctor.lean 12 declarations
- QuasitraceQuotientHomogeneity.lean 4 declarations
- QuasitraceQuotientIteration.lean 3 declarations
- QuasitraceQuotientMetric.lean 19 declarations
- QuasitraceQuotientMetricLimits.lean 5 declarations
- QuasitraceQuotientMetricOperations.lean 5 declarations
- QuasitraceQuotientNorm.lean 17 declarations
- QuasitraceQuotientNormContinuity.lean 4 declarations
- QuasitraceQuotientOrder.lean 6 declarations
- QuasitraceQuotientOrthogonal.lean 2 declarations
- QuasitraceQuotientOrthogonalSums.lean 1 declarations
- QuasitraceQuotientRealImag.lean 6 declarations
- QuasitraceQuotientRickart.lean 2 declarations
- QuasitraceQuotientRootCauchy.lean 7 declarations
- QuasitraceQuotientRootProjection.lean 3 declarations
- QuasitraceQuotientSpectralCuts.lean 4 declarations
- QuasitraceQuotientSpectralOrder.lean 3 declarations
- QuasitraceQuotientSpectralProducts.lean 4 declarations
- QuasitraceQuotientSpectralProjection.lean 1 declarations
- QuasitraceQuotientStar.lean 6 declarations
- QuasitraceQuotientSupport.lean 3 declarations
- QuasitraceQuotientValue.lean 9 declarations
- QuasitraceQuotientValueMetricLimits.lean 2 declarations
- QuasitraceScaledRank.lean 1 declarations
- QuasitraceSelfAdjoint.lean 12 declarations
- QuasitraceSelfAdjointLimits.lean 3 declarations
- QuasitraceSqrtAddition.lean 1 declarations
- QuasitraceUltralimitComplex.lean 2 declarations
- QuasitraceUltralimitPositive.lean 17 declarations
- QuasitraceUltralimitSize.lean 14 declarations
- QuasitraceUltraproductAWEmbedding.lean 14 declarations
- QuasitraceUnitary.lean 3 declarations
- QuasitraceValueLimits.lean 2 declarations
- QuasitraceWeightedAddition.lean 3 declarations
- TwoQuasitraceBounds.lean 3 declarations