OAI/Analysis/MarkovType/SmoothRenormed.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MarkovSuperreflexivity.symmetricPowerSmoothWith_renormed line 11
2. theorem OAI.MarkovSuperreflexivity.normPowerSmoothWith_renormed line 22
3. theorem OAI.MarkovSuperreflexivity.markovTypeWith_of_equivalent_symmetricPowerSmooth line 32
4. theorem OAI.MarkovSuperreflexivity.markovTypeWith_of_equivalent_powerSmooth line 40
5. theorem OAI.MarkovSuperreflexivity.hasNontrivialMarkovType_of_equivalent_symmetricPowerSmooth line 48
6. theorem OAI.MarkovSuperreflexivity.hasNontrivialMarkovType_of_equivalent_powerSmooth line 55