OAI/Probability/SKFluctuations/RawLossLogarithms.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

Raw Loss Logarithms.

  1. theorem OAI.SKFluctuations.tendsto_raw_log_margin line 15
  2. def OAI.SKFluctuations.PhysicalBandWindow.generalFarBaseConstant line 27
  3. theorem OAI.SKFluctuations.PhysicalBandWindow.generalScaleFactor_log_bound line 30
  4. theorem OAI.SKFluctuations.tendsto_raw_balanced_margin line 81
  5. theorem OAI.SKFluctuations.PhysicalBandWindow.loss_le_half_scale line 97
  6. theorem OAI.SKFluctuations.PhysicalBandWindow.eventually_coefficient_small line 113
  7. theorem OAI.SKFluctuations.physicalReadyRetainedWindow line 144
  8. theorem OAI.SKFluctuations.physicalSusceptibility_bound line 250
  9. theorem OAI.SKFluctuations.physicalSusceptibility_measurable line 261
  10. theorem OAI.SKFluctuations.physicalCutSusceptibility_measurable line 279
  11. theorem OAI.SKFluctuations.physicalCutSusceptibility_bound line 296
  12. theorem OAI.SKFluctuations.physicalCutSusceptibility_memLp line 316
  13. def OAI.SKFluctuations.Hierarchy.terminalScore line 339
  14. theorem OAI.SKFluctuations.Hierarchy.terminalScore_integrable line 342
  15. theorem OAI.SKFluctuations.Hierarchy.condExp_terminalScore_self line 356
  16. theorem OAI.SKFluctuations.Hierarchy.condExp_terminalScore line 379
  17. theorem OAI.SKFluctuations.Hierarchy.integral_terminalScore line 391
  18. def OAI.SKFluctuations.Hierarchy.terminalWindow line 400
  19. theorem OAI.SKFluctuations.Hierarchy.terminalWindow_integrable line 404
  20. theorem OAI.SKFluctuations.Hierarchy.condExp_terminalWindow line 411
  21. theorem OAI.SKFluctuations.Hierarchy.sqnorm_le_condExp_window line 441
  22. theorem OAI.SKFluctuations.Hierarchy.momentNorm_le_of_norm_le line 473
  23. theorem OAI.SKFluctuations.Hierarchy.momentNorm_smul line 483
  24. theorem OAI.SKFluctuations.Hierarchy.momentNorm_condExp_le line 489
  25. theorem OAI.SKFluctuations.Hierarchy.momentNorm_centering_le line 497
  26. theorem OAI.SKFluctuations.Hierarchy.terminalScore_memLp line 515
  27. theorem OAI.SKFluctuations.Hierarchy.terminalWindow_memLp line 538
  28. theorem OAI.SKFluctuations.Hierarchy.window_square_moment_le line 545
  29. theorem OAI.SKFluctuations.Hierarchy.momentNorm_nat_eq line 584
  30. theorem OAI.SKFluctuations.Hierarchy.momentNorm_sqnorm_nat line 594
  31. theorem OAI.SKFluctuations.physical_radius_window_integral_memLp line 614
  32. theorem OAI.SKFluctuations.physical_radius_window_energy_moment line 635
  33. theorem OAI.SKFluctuations.physical_sqnorm_memLp line 662