Research proof index

Search theorem names, mathematical ideas, modules, topics, projects, and role-labelled researchers. Open a result for its complete indexed Lean declaration and source record.

This index contains 115 research declarations. Search 10,000 more complete Mathlib declarations.

Search proofs

All topics

Search topics

ABC conjectureabstractabstract lang completenessactionadditive combinatoricsadele ringadic valuationaffine groupaffine spacesahiv22ahiv22supportalgebraic geometryalgorithmallow denyallows termalmost orthogonalityalmost periodicityanalysisanalytic number theoryanalytic setangular momentumangular velocityantichain operatorantichain tile countappendapprox hom pfrapproximationarcaritharithmetic geometryarithmetic progressionsas tensorasymptoticsasync runtimeauthorizationauthorizeauthorizerautomata theoryautomorphismauxiliaryball extensionball scalingbase changebase permbasicbasicsbasisbasis linearbatched evaluatorbehavioural theoryberlekamp welchbig opbijectivitybilinear formbindingbirthdaybisimulationbivariateblock rel distancebmobn254borel caratheodorybounding mutualbraketbridgebrownian motionbrun titchmarshbuchi congrbuchi congruencebuchi interbundledbundled semanticscaching logging oraclecaching oraclecadlagcadlag modificationcalculationscampanatocan reach viacanonicalcapacitycardinalitycarleson huntcarleson hunt basiccarleson on the real line basiccarleson on the real line continuouscarleson operator realcategory theorycell refchainchangcheck claimchernoffchiral indiceschoueka lemmachurchclass dclass field theoryclassical carlesonclifford algebracma to nmaco psetcoding theorycollisioncollision resistancecombinatoricscombinecommutationcommutative algebracompactcompact hausdorff ringscompact systemcompatibilitycompiled policiescompilercompletenesscompletionscomplexity theorycompositioncomputabilitycomputer scienceconcatconclusionsconcretecondconfluencecongrconsensusconsequencesconsistencyconstantconstant slice distconstant time distconstructionscontinuitycontractioncontractionscontrol approximation effectcontrol approximation effect basiccontrol approximation effect continuousconversionconvolutioncoordinatecore interaction phasecorrectnesscorrugationcostcost accountingcost modelcounter modelcovariancecross productcryptographycurlcutoff admissibilitycyclotomic fieldsdebutdecoderdecoding radiusdedekind mac neille completiondeferred samplingdefsdegree conflictdeltaderivativederivativesdetdet concatdet muller langdetailsdeterministicdifferential geometrydiffie hellmanDiophantine equationsdirichlet kerneldisagreementdiscretedist equivdist of functiondistancedistributiondivdivergence of setsdomaindoob lpdoob meyerdoubling measuredown singletdpidrcdualdual pairdyn systeme2eagereager tableeffective potentialeigenfunctioneisensteineisenstein asymptoticselectric fieldelliptic coefficientsembeddingempotentialendgameenergyenforcementenforcerensembleentanglemententropyentropy pfrequation1323equation677equational logicestimateeuler lagrangeeuler maclaurineuler mascheroni boundseval disteval splitevaluationevaluation binding conflictevaluatorexamplesexceptional setexecutionexistenceexistence theoryexpected costexponential integrabilityexponential mapextractabilityextractorfactorizationfair schedulerFermat's Last Theoremfgfibringfidelityfieldfield strengthfinitary carlesonfinitefinite adele ringfinite coverfinite dimensionalfinite fieldfinitenessfinset termsfirstfirst estimatefive quantaflattenflex approxfoldingfolding polynomialforest complementforest unionforestsforkformal languagesformal logicfoundationsfourierFourier analysisfree semigroupfree statefrey packagefrobeniusfrom mathlibfrom unaryfull beta confluencefull beta eta confluencefull etafunctiongadgetsgauge transformationgen heapgen setsgeneralgeneralizedgenerate seedgeneric liftghost mapgradgradinggrid structuregromovgroupgroup theory stuffguruswamiguruswami sudanhaltinghamiltonianhandler from unaryhandler specsharmonic analysisharmonic waveharnackhas tauhas var adjointhash commitmentheat kernelheat solutionheat solution propertyhelperherbrand quotienthilbert kernelhilbert strong typehilbert94histholder normholder van der corputhom pfrhomotopyhopshprinciplehundred percenthypothesis testingideal gasidentical until badimmersionimplimplicationsimproved pfrindicatorinduction scheme delta1inductive constructionsinequalitiesinf modelinf occinfinite graph ramseyinfinite wireinflationinputinsert and contractinsert and contract natinsert noneinsert someinsertion sortinstanceinstancesintegralintegral closureinteractive protocolsinterleaved codeintervalinverse iterationis dist boundedis extremais plane waveis viableisqbridgeiteriterated laplacianiterationiwaniec kowalski ch1kemdemkey encap mechkinetic energykinetic termknowledge soundnesskoszul signkullbackkummers lemmal2estimatelagrangianlanguagelaplace inversionlaplace runge lenz vectorlarge separationleakagelemmaslevelslex'orderlie traceline in cubiclinear codelinear mv extensionlinearizedlinftylipschitz normlistlocallocal fieldslocal john nirenberglocalisation datalocallyloglog gradientlogging oraclelooplp function toolkitls corelyubashevsky seilermac from prfmachinemagnetic fieldmainmain resultsmain theoremmain thmmapmap unionmarcinkiewicz zygmundmatrix derivativesmatrix divmatrix mapmaximal inequalitymcageneratormdifferentiablemdscodemeasure theorymedium pntmellin calculusmetatheorymetricmicciancio youngmin layer tilesminimal super setmllmodel datamodular formsmodulemodulesmomentummon predmore ruzsa distmotionmstatemulti appmulti tau functionalmultilinearmultiplicationmyhill nerodenavier stokesnegligibleno entities errornon deterministicnontangential operatornormnorm boundnorm pownormal ordernormsnumber theoryobelixobservation oracleof envof finsetof potential termofeoi2omega executionomega languageomega reg langomega regular languageone dimensionone jet bundleoperatorsopsoptoptionoptional samplingoracleorderpackingpadicpairparameterizationparametric hprinciplepartial differential equationspartial mapperfect secrecypermutative extensionperron formulapheno closedpheno constrainedphi transformphys hermitephysicspick subsetpinchingpmfpointwise estimatepolicypolicy slicepolynomialpositionpositive partpositive part preludepotentialprepre estimatepre iterationprelimspreludepreserves invpreserves type ofprime numbersprimrec codingprobabilityprobe epsprodproductprogram logicprogram semanticsprogram verificationprogramming oracleproof dataproof systemsproof theoryproperpropertiesproximity generatorspsetpsipublic estimateqpquadratic twistsquantative estimatequantitativequantum channelsquantum field theoryquantum informationquark doubletquery boundquicksortquotientradial angular measureramanujan identitiesrandom queryrational functionsreachablereal complexrectanglerectangle argument principlerecurrencerecursionreduce claimreductionreduction base changereductionsreed solomonrefutabilityreg langregular languageregularity theoryregularizedregularized energyregularized witnessesreindexingrelrelationrelationsrelativerelative distancerelativityremaining tilesreparametrizationreplay forkres to imag axisresidualresidue calc on rectanglesresolventresource profileresponderrestrict degreerestrict degree varrestricted provabilityrestricted weak typerestrictionresultantresultsrho functionalrough inputround consistencyrowsrqrudinsafetysampleable typesamplingscaled ball estimatesschur triangulationschwartz submoduleschwartz zippel countingsec expsecond estimatesection2section4securityseeded forkseeded oraclesegmentself adjointsemanticssend challengesend claimsend witnessseparation logicseq composeserre approximationserre derivative slashsetset theoryshamirsigmasignature algsimple processsimulate qsimulationsinc kernel error boundssingle roundslash action auxilslicesmooth approximationsmooth embeddingsmooth existencesmooth testssobolevsobolev poincaresobolev spacessolid spheresolutionsoundnessspectral projection boundsphere packingsplit foldsplit multiplicative reductionsplitting modulesquare integrablessastage onestampacchia truncationstandard formstandard reductionstate projectionstate separatingstatementstatic contractstatic wick termstd do bridgestepsstochastic intervalstochastic processesstr actionstraight linestrong normstrong pntstructuressub specsubdomainsubtypesucc succ abovesumsumcheck phasesuper commutesupportsurroundingsymbolic compilationsymbolizersymm enc algsymmetrictake droptanhtate curvetate curve base changetate curve constructiontate parametertau functionaltau in queriesten quantatensor producttensorialtest functionsthermo quantitiesthree apthree dimensiontile correlationtile existencetile structuretime contracttime contractiontime liketime ordertime slicetiseto complexto fft domainto nato singleto single acceptto solstopologytorsion endgametotaltotal derivative equivalencetpetracetrace inner producttrace vanishingtrajectorytraversaltrivial cohomologytriviality criteriontruncationttransformtvdisttwotwo statetypecheckertypecheckingtypingudfultraproductunaryunbalancingunboundedunbundleduncertaintyuncontracted listuniform integrableuniquenessunitunit tensorunitaryuniversal algebraunpredictabilityunramifiedup downup singletupdatesutransformvalid refsvalidationvan der corputvandermondevariancevcdimensionvector bundlesverificationverifierversion spaceversion space latticeweak calderon zygmundweak derivativeweak derivativesweak harnackweak pfrweightedweighted estimateswell typedwell typed okwell typed verificationwfwhole space sobolevwick contractionswick termwicks theorem normalwienerwired runwith abortwitnesseswriter costyukawazero consensuszero count crudezeta boundszf

Source projectLean version

115 results

Clear filters

Project-declaredLean 4.28.0

W mat sq le one

W_mat_sq_le_one

Plain-language statement

Core inequality: W†W ≤ I. This is the key step, following from the isometry argument: V_rho ⊗ I_C and I_A ⊗ V_sigma are isometries, their cross product has norm ≤ 1, and the result can be related to W_mat through the MES computation (Eq. 6 in Lin-Kim-Hsieh).

quantum informationentropyquantum channels

Source project: quantumInfo

Person-level attribution pending.

View proof record

1…20

1…19 20

Page 20 of 20

therefore

Search complete Lean declarations, inspect their provenance, and check code in a live Lean environment.

Research

Research proofs Open problems Search Mathlib Type and shape search Projects Researchers

Use Therefore

Check a proof Packages MCP, API, and editor Verification model

Built for the Lean community.Verification, provenance, and authorship stay separate.