OAI/Probability/SKRatio/Variational/FormContinuity.lean
8 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.SKRatio.Planted.weightedForm_field_subline 15 - lemma
OAI.SKRatio.Planted.weightedForm_field_boundline 21 - lemma
OAI.SKRatio.Planted.diagonalForm_field_boundline 31 - lemma
OAI.SKRatio.Planted.weightedForm_variance_eqline 56 - lemma
OAI.SKRatio.Planted.weightedForm_variance_field_boundline 61 - lemma
OAI.SKRatio.Planted.compactForm_field_boundline 84 - lemma
OAI.SKRatio.Planted.form_kernels_uniformline 109 - lemma
OAI.SKRatio.Planted.compactForm_uniform_field_changeline 134