OAI/Probability/SKBarriers/Replicas/ReplicaVarianceSplit.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SK.Analytic.finiteReplicaMoment_const line 18
2. theorem OAI.SK.Analytic.finiteReplicaMoment_add line 22
3. theorem OAI.SK.Analytic.finiteReplicaMoment_const_mul line 26
4. theorem OAI.SK.Analytic.finiteReplicaMoment_sub_square line 33
5. theorem OAI.SK.Analytic.finiteReplicaMoment_variance_split line 41
6. theorem OAI.SK.Analytic.finiteReplicaMoment_normalizedDot line 47
7. theorem OAI.SK.Analytic.finiteCovariance_trace_square_nonneg line 54
8. theorem OAI.SK.Analytic.finiteReplica_normalized_variance_le line 60