OAI/Probability/FreeIsing/Estimates/ComponentFusionRecurrence.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem367.HasFreeIsingLaw.selected_child_parent_abs_le line 19
2. theorem OAI.Problem367.HasFreeIsingLaw.selected_child_parent_secondMoment line 36
3. def OAI.Problem367.gaussianComponentInformation line 60
4. theorem OAI.Problem367.HasFreeIsingLaw.gaussian_component_information_fusion line 67
5. theorem OAI.Problem367.HasFreeIsingLaw.gaussian_component_critical_information_upper line 161