OAI/Probability/SKGap/Stability/FieldIntegralReduction.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SKGap.fieldMollifier line 16
  2. def OAI.SKGap.fieldIntegral line 20
  3. lemma OAI.SKGap.continuous_fieldMollifier line 24
  4. def OAI.SKGap.conditionalFieldWeight line 30
  5. lemma OAI.SKGap.field_noise_convolution line 35
  6. theorem OAI.SKGap.field_reduction_fixed line 50
  7. lemma OAI.SKGap.fieldMollifier_eq_localAction line 94
  8. lemma OAI.SKGap.fieldIntegral_eq_localVolume line 101
  9. lemma OAI.SKGap.outer_add_rank_le_two line 117
  10. lemma OAI.SKGap.operator_outer_vector_le line 128
  11. lemma OAI.SKGap.vectorNorm_const_one line 132
  12. lemma OAI.SKGap.spinVariance_norm_bound line 137
  13. lemma OAI.SKGap.weightedMagnetization_norm_bound line 148
  14. def OAI.SKGap.plantedJacobianPerturbation line 154
  15. lemma OAI.SKGap.plantedJacobianPerturbation_rank line 158
  16. lemma OAI.SKGap.plantedJacobianPerturbation_norm line 168
  17. lemma OAI.SKGap.fieldJacobian_planted_formula line 194