`OAI/Analysis/SeparableQuotients/`

1480 declarations, 0 contain sorry, 0 declared as axioms; 76 files

Folders

Positive/ 25 files, 249 declarations

Files

AdjointSurjectivity.lean 5 declarations
BlockApproximation.lean 35 declarations
BlockEstimates.lean 16 declarations
BoundedCompleteness.lean 27 declarations
BranchPaths.lean 53 declarations
BranchReduction.lean 18 declarations
BranchSeparation.lean 12 declarations
ChangedPredual.lean 17 declarations
CoherentClosures.lean 41 declarations
ColorDecomposition.lean 29 declarations
Complexification.lean 25 declarations
CoordinateDual.lean 27 declarations
CoordinatePredual.lean 50 declarations
EvaluationCriterion.lean 5 declarations
ExactPairs.lean 7 declarations
FiniteLp.lean 26 declarations
FiniteNormers.lean 21 declarations
LpDuality.lean 20 declarations
Main.lean 1 declarations
MarkedEstimates.lean 19 declarations
Model.lean 4 declarations
NegativeComplex.lean 4 declarations
NegativeReal.lean 1 declarations
NormCompletion.lean 44 declarations
NormingBounds.lean 23 declarations
NormingFamilies.lean 36 declarations
NormingOperations.lean 42 declarations
NormingTrees.lean 33 declarations
Parameters.lean 47 declarations
PartitionBlocks.lean 29 declarations
PathCoding.lean 39 declarations
PathConvergence.lean 27 declarations
PathLimits.lean 38 declarations
PathOperators.lean 38 declarations
PathRigidity.lean 30 declarations
PathStabilization.lean 26 declarations
PerturbationOperator.lean 29 declarations
PrefixNormers.lean 50 declarations
ProductQuotients.lean 4 declarations
QuotientPerturbation.lean 13 declarations
RamseyThinning.lean 7 declarations
RealCoefficients.lean 5 declarations
SeparableSubspaces.lean 5 declarations
StoppedCharges.lean 32 declarations
StrictSingularity.lean 39 declarations
TailBlocks.lean 32 declarations
TreeBounds.lean 22 declarations
TreeCharges.lean 22 declarations
WindowCharges.lean 18 declarations
WindowEstimates.lean 16 declarations
WindowThinning.lean 22 declarations