OAI/Probability/Perceptron/Variational/BoundedC1.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SphericalPerceptronFreeEnergy.BoundedC1 line 21
  2. lemma OAI.SphericalPerceptronFreeEnergy.BoundedC1.zero line 23
  3. lemma OAI.SphericalPerceptronFreeEnergy.BoundedC1.add line 25
  4. lemma OAI.SphericalPerceptronFreeEnergy.BoundedC1.smul line 31
  5. lemma OAI.SphericalPerceptronFreeEnergy.BoundedC1.heatTilt line 36
  6. lemma OAI.SphericalPerceptronFreeEnergy.heatGenerator_boundedC1 line 42
  7. structure OAI.SphericalPerceptronFreeEnergy.HeatIntervalParam line 45
  8. def OAI.SphericalPerceptronFreeEnergy.parametricHeatJet line 50
  9. def OAI.SphericalPerceptronFreeEnergy.parametricHeatVelocity line 54
  10. lemma OAI.SphericalPerceptronFreeEnergy.parametricHeatVelocity_boundedC1 line 60
  11. lemma OAI.SphericalPerceptronFreeEnergy.parametricHeatJet_hasDerivAt line 68
  12. lemma OAI.SphericalPerceptronFreeEnergy.heatLog_boundary_hasDerivAt line 82
  13. lemma OAI.SphericalPerceptronFreeEnergy.weighted_list_tail_nonneg line 117
  14. def OAI.SphericalPerceptronFreeEnergy.heatBoundaryTerms line 139
  15. def OAI.SphericalPerceptronFreeEnergy.heatBoundarySum line 148
  16. lemma OAI.SphericalPerceptronFreeEnergy.heatBoundarySum_cons line 151
  17. lemma OAI.SphericalPerceptronFreeEnergy.heatGenerator_sub line 167
  18. def OAI.SphericalPerceptronFreeEnergy.firstHeatGenerator line 175
  19. lemma OAI.SphericalPerceptronFreeEnergy.parametricHeatVelocity_boundary line 180
  20. lemma OAI.SphericalPerceptronFreeEnergy.heatBoundaryTerms_lower line 216
  21. lemma OAI.SphericalPerceptronFreeEnergy.heatBoundaryTerms_ordered line 237
  22. lemma OAI.SphericalPerceptronFreeEnergy.heatBoundarySum_nonneg line 256
  23. lemma OAI.SphericalPerceptronFreeEnergy.parametricHeatJet_deriv_nonpos line 278
  24. lemma OAI.SphericalPerceptronFreeEnergy.heatLogBCF_time_continuousAt_all line 293
  25. lemma OAI.SphericalPerceptronFreeEnergy.heatLogBCF_terminal_norm_le line 323
  26. lemma OAI.SphericalPerceptronFreeEnergy.heatLogBCF_moving_continuousAt line 334
  27. lemma OAI.SphericalPerceptronFreeEnergy.parametricHeatJet_continuousAt line 356
  28. lemma OAI.SphericalPerceptronFreeEnergy.parametricHeatJet_tail_order line 367
  29. lemma OAI.SphericalPerceptronFreeEnergy.poissonWeightedTotal_law line 389