OAI/Probability/FreeIsing/Posterior/InteriorLocalization.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem367.PosteriorInteriorLocalization.field_bound_iff_tanh_bounds line 13
  2. theorem OAI.Problem367.PosteriorInteriorLocalization.continuous_tanh line 32
  3. theorem OAI.Problem367.PosteriorInteriorLocalization.ae_all_field_bound_of_continuous line 35
  4. theorem OAI.Problem367.PosteriorInteriorLocalization.continuous_artanh_of_interior line 61
  5. theorem OAI.Problem367.PosteriorInteriorLocalization.exists_uniform_radius_of_compact line 69
  6. theorem OAI.Problem367.PosteriorInteriorLocalization.inverse_variance_le_of_abs_le line 79
  7. def OAI.Problem367.PosteriorInteriorLocalization.radius line 90
  8. theorem OAI.Problem367.PosteriorInteriorLocalization.radius_nonneg line 92
  9. theorem OAI.Problem367.PosteriorInteriorLocalization.radius_lt_one line 99
  10. theorem OAI.Problem367.PosteriorInteriorLocalization.radius_monotone line 104
  11. theorem OAI.Problem367.PosteriorInteriorLocalization.tendsto_radius line 112
  12. theorem OAI.Problem367.PosteriorInteriorLocalization.eventually_uniform_abs_lt_radius line 120
  13. theorem OAI.Problem367.PosteriorInteriorLocalization.ae_compact_localization_of_field_bound line 129
  14. def OAI.Problem367.PosteriorInteriorLocalization.sampledRadiusEvent line 146
  15. theorem OAI.Problem367.PosteriorInteriorLocalization.measurableSet_sampledRadiusEvent line 149
  16. theorem OAI.Problem367.PosteriorInteriorLocalization.sampledRadiusEvent_monotone line 156
  17. theorem OAI.Problem367.PosteriorInteriorLocalization.mem_sampledRadiusEvent_iff line 162
  18. theorem OAI.Problem367.PosteriorInteriorLocalization.ae_mem_iUnion_sampledRadiusEvent line 171
  19. theorem OAI.Problem367.PosteriorInteriorLocalization.tendsto_measure_sampledRadiusEvent line 182
  20. theorem OAI.Problem367.PosteriorInteriorLocalization.tendsto_measure_compl_sampledRadiusEvent line 195