OAI/Probability/FreeIsing/Ising/CavityTailTransport.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem367.IsingCavityTailTransport.cavityObservable_identDistrib_relabel line 20
2. theorem OAI.Problem367.IsingCavityTailTransport.cavityObservable_identDistrib_root_component line 36
3. theorem OAI.Problem367.IsingCavityTailTransport.exists_cavityObservable_identDistrib_root_component line 62
4. theorem OAI.Problem367.IsingCavityTailTransport.cavityObservable_tail_le_of_component_tails line 88
5. theorem OAI.Problem367.IsingCavityTailTransport.logVariance_small_time_of_component_tails line 102