OAI/Probability/GaussianInformation/Dyadic/StateExpectation.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RepeatedLocalization.FiniteChannel.expectation line 21
  2. lemma OAI.RepeatedLocalization.FiniteChannel.expectation_const line 24
  3. lemma OAI.RepeatedLocalization.FiniteChannel.expectation_add line 28
  4. lemma OAI.RepeatedLocalization.FiniteChannel.expectation_const_mul line 32
  5. lemma OAI.RepeatedLocalization.FiniteChannel.expectation_mono line 36
  6. lemma OAI.RepeatedLocalization.FiniteChannel.sum_mass_dbind line 40
  7. lemma OAI.RepeatedLocalization.FiniteChannel.expectation_dbind line 48
  8. lemma OAI.RepeatedLocalization.FiniteChannel.expectation_dbind_fst line 57
  9. lemma OAI.RepeatedLocalization.FiniteChannel.expectation_bind_fst line 65
  10. lemma OAI.RepeatedLocalization.FiniteChannel.bind_positive_parent line 77
  11. lemma OAI.RepeatedLocalization.FiniteChannel.dbind_positive_parent line 84
  12. lemma OAI.RepeatedLocalization.FiniteChannel.dbind_positive_conditional line 91
  13. lemma OAI.RepeatedLocalization.zero_heavy_refinement line 101
  14. structure OAI.RepeatedLocalization.AnalysisState line 129
  15. def OAI.RepeatedLocalization.AnalysisState.information line 145
  16. def OAI.RepeatedLocalization.AnalysisState.depth line 146
  17. def OAI.RepeatedLocalization.AnalysisState.concentration line 147
  18. def OAI.RepeatedLocalization.AnalysisState.potential line 148
  19. lemma OAI.RepeatedLocalization.AnalysisState.depth_nonneg line 151
  20. lemma OAI.RepeatedLocalization.AnalysisState.concentration_nonneg line 154
  21. lemma OAI.RepeatedLocalization.AnalysisState.information_lower line 157
  22. lemma OAI.RepeatedLocalization.AnalysisState.information_of_potential line 184
  23. lemma OAI.RepeatedLocalization.scorePosterior_one line 198
  24. lemma OAI.RepeatedLocalization.cubePrior_spread_root line 201
  25. def OAI.RepeatedLocalization.initialState line 216
  26. lemma OAI.RepeatedLocalization.initialState_potential line 236
  27. lemma OAI.RepeatedLocalization.posterior_cube_domination line 241
  28. def OAI.RepeatedLocalization.appendHistoryEquiv line 252
  29. lemma OAI.RepeatedLocalization.appendHistoryEquiv_apply line 255
  30. def OAI.RepeatedLocalization.initRules line 258
  31. lemma OAI.RepeatedLocalization.past_snoc_castSucc line 261
  32. lemma OAI.RepeatedLocalization.past_snoc_last line 267
  33. lemma OAI.RepeatedLocalization.historyLikelihood_snoc line 273
  34. lemma OAI.RepeatedLocalization.historyLikelihood_sum line 281
  35. def OAI.RepeatedLocalization.blockChannel line 290
  36. def OAI.RepeatedLocalization.historyChannel line 296