OAI/Probability/SpanningForest/TransferCurrent.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem336.TransferCurrent.bilinear line 16
  2. lemma OAI.Problem336.TransferCurrent.bilinear_symmetric line 20
  3. lemma OAI.Problem336.TransferCurrent.inverse_symmetric line 24
  4. lemma OAI.Problem336.TransferCurrent.bilinear_rankOne line 29
  5. def OAI.Problem336.TransferCurrent.bilinearCLM line 35
  6. lemma OAI.Problem336.TransferCurrent.bilinearCLM_apply line 45
  7. lemma OAI.Problem336.TransferCurrent.hasDerivAt_inverse_affine line 48
  8. lemma OAI.Problem336.TransferCurrent.bilinear_neg line 60
  9. lemma OAI.Problem336.TransferCurrent.bilinear_smul line 65
  10. lemma OAI.Problem336.TransferCurrent.hasDerivAt_bilinear_inverse_affine line 69
  11. lemma OAI.Problem336.TransferCurrent.hasDerivAt_transfer_rankOne line 77
  12. lemma OAI.Problem336.TransferCurrent.transfer_response_nonpos line 91
  13. lemma OAI.Problem336.TransferCurrent.hasDerivAt_transfer_logWeight line 96
  14. lemma OAI.Problem336.TransferCurrent.hasDerivAt_transfer_logWeight_self line 108
  15. def OAI.Problem336.TransferCurrent.laplacian line 124
  16. def OAI.Problem336.TransferCurrent.shift line 127
  17. lemma OAI.Problem336.TransferCurrent.laplacian_symmetric line 131
  18. lemma OAI.Problem336.TransferCurrent.laplacian_shift line 136
  19. def OAI.Problem336.TransferCurrent.marginal line 155
  20. lemma OAI.Problem336.TransferCurrent.hasDerivAt_marginal_shift_of_ne line 158
  21. lemma OAI.Problem336.TransferCurrent.hasDerivAt_marginal_shift_self line 167
  22. lemma OAI.Problem336.TransferCurrent.deriv_marginal_shift_nonpos line 176
  23. lemma OAI.Problem336.TransferCurrent.sum_weighted_transfer_sq line 184
  24. def OAI.Problem336.TransferCurrent.responseSquare line 207
  25. lemma OAI.Problem336.TransferCurrent.responseSquare_nonneg line 212
  26. lemma OAI.Problem336.TransferCurrent.responseSquare_self line 217
  27. lemma OAI.Problem336.TransferCurrent.sum_responseSquare line 223
  28. lemma OAI.Problem336.TransferCurrent.marginal_nonneg line 231
  29. lemma OAI.Problem336.TransferCurrent.marginal_le_one line 237
  30. def OAI.Problem336.TransferCurrent.response line 244
  31. lemma OAI.Problem336.TransferCurrent.response_self line 247
  32. lemma OAI.Problem336.TransferCurrent.response_ne_nonpos line 252
  33. lemma OAI.Problem336.TransferCurrent.hasDerivAt_marginal_shift line 257
  34. lemma OAI.Problem336.TransferCurrent.sum_response line 267
  35. lemma OAI.Problem336.TransferCurrent.sum_abs_response line 272
  36. lemma OAI.Problem336.TransferCurrent.sum_abs_deriv_marginal_le_half line 292