OAI/Probability/SKValue/GroundState/CascadePassage.lean
10 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.SKValueG.finite_step_guerra_upperline 12 - def
OAI.SKValueG.profileTreeline 43 - lemma
OAI.SKValueG.profileTree_validline 47 - lemma
OAI.SKValueG.profileTree_scaleline 54 - lemma
OAI.SKValueG.profileTree_valueline 63 - lemma
OAI.SKValueG.coleHopf_mono_lipschitzline 70 - lemma
OAI.SKValueG.profileTree_le_smoothline 81 - lemma
OAI.SKValueG.patchTime_integralline 94 - lemma
OAI.SKValueG.profile_weighted_integrableline 105 - lemma
OAI.SKValueG.profileTree_correctionline 109