IndisputableMonolith.Gravity.SevenGaps.Gap2PoissonCoarea · Recognition explainer

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Gravity.SevenGaps.Gap2MeasureDerivation module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.SevenGaps.Gap2JEhrhartSpan module_import

declarations in this module (82)

structure TetFree L69
def emptyTF L77
def vertexUnused L85
def postVertex L89
def unpostMaxVertex L100
def postEdge L121
def unpostMaxEdge L134
def moveRate L145
def sortRespectingArrivalCount L149
def orderErasureWeight L155
theorem postVertex_nV L162
theorem postEdge_nE L165
theorem unpostMaxEdge_nE L168
theorem postEdge_unpost_nE L172
theorem moveRate_symm_lifo_vertex L180
theorem moveRate_symm_lifo_edge L185
def uniformNamed L191
theorem uniform_detailed_balance_of_rate_symm L199
theorem moveRate_symm L208
theorem uniform_detailed_balance L211
structure Cap3Tally L229
def measuredCap3 L243
theorem measuredCap3_nStates L256
theorem measuredCap3_irreducible L257
theorem measuredCap3_symmetric L260
theorem measuredCap3_pi L261
theorem measuredCap3_small_ge L263
theorem measuredCap3_decoy L267
theorem measuredCap3_sj_decoy L268
theorem cap3_stationary_is_uniform L273
def pathPlusIsolated L289
theorem pathPlusIsolated_counts L299
theorem twoEdge_counts L303
def edgeCommOK L310
def twoEdgeEV L314
def pathPlusEV L317
def twoEdgeAutCount L321
def pathPlusAutCount L326
theorem twoEdge_autCount_eq_two L330
theorem pathPlus_autCount_eq_one L331
def inFibre L335
def twoEdgeFibre L340
def pathPlusFibre L345
theorem twoEdge_fibre_card L350
theorem pathPlus_fibre_card L353
abbrev NamedPi L365
def classMassPi L368
def uniformPi L373
theorem classMassPi_of_uniform L377
def classMassRatioPi L385
def UniformNamedPremise L395
theorem classMassRatioPi_of_uniform_eq_fibre_ratio L399
theorem classMassRatioPi_of_uniform_eq_half L415
def classMassRatio_420 L424
theorem classMassRatio_420_eq_half L427
theorem autInverseRatio_eq_half L432
theorem fibre_ratio_eq_aut_inverse_ratio L439
def SJ_twoEdge L447
def SJ_pathPlus L448
theorem SJ_twoEdge_rfl L450
theorem SJ_pathPlus_rfl L451
def predictedRatio_qSJ L455
theorem predictedRatio_qSJ_at_one L458
theorem predictedRatio_qSJ_at_two L461
def residualOverHalf L467
theorem residualOverHalf_eq_one L470
theorem deltaCounts_zero L475
theorem residual_family_silent L488
theorem arrivalCount_420 L501
theorem twoEdge_fibre_eq_orders_div_aut L505
theorem pathPlus_fibre_eq_orders_div_aut L511
theorem coarea_at_twoEdge L519
theorem coarea_at_pathPlus L526
structure PoissonCoareaIndex L535
def poissonCoareaIndex L551
theorem index_firewall L560
theorem index_cap3 L561
theorem index_ratio L562
theorem index_residual L563
theorem index_coarea L564

… and 2 more