OAI/Probability/FreeIsing/Gaussian/TreeResponseRootPosterior.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem367.GaussianTreeResponse.integrable_shiftedRow_sq_anyroot line 15
  2. theorem OAI.Problem367.GaussianTreeResponse.integral_shiftedRow_sq_le_distance line 41
  3. theorem OAI.Problem367.GaussianTreeResponse.integrable_observedRow_sq_anyroot line 68
  4. theorem OAI.Problem367.GaussianTreeResponse.integral_observedRow_sq_le_distance line 80
  5. theorem OAI.Problem367.HasFreeIsingLaw.finiteObservation_posteriorResponse_sq_bound_distance line 104
  6. theorem OAI.Problem367.HasFreeIsingLaw.gaussian_posteriorResponse_sq_decay_distance line 125
  7. theorem OAI.Problem367.HasFreeIsingLaw.gaussian_posteriorResponse_row_energy_anyroot line 145
  8. theorem OAI.Problem367.HasFreeIsingLaw.gaussian_posteriorResponse_row_energy_tail_anyroot line 188