def definition def or abbrev

`overlap`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  20def overlap (K : MarkovKernel ι) (i i' : ι) : ℝ := ∑ j, min (K.P i j) (K.P i' j)

Definition body.

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

eleven_congruence_not_mock in IndisputableMonolith.Mathematics.RamanujanBridge.CongruenceQ3Bridge decl_use
mock_and_congruence_unified_by_Q3 in IndisputableMonolith.Mathematics.RamanujanBridge.CongruenceQ3Bridge decl_use
mock_closure_periods_div_8 in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
modal_nyquist in IndisputableMonolith.Modal.ModalGeometry decl_use
C1_scope in IndisputableMonolith.Papers.ClaimBoundaries decl_use
vcb_derived in IndisputableMonolith.Physics.MixingDerivation decl_use
cabibbo_radiative_correction in IndisputableMonolith.Physics.MixingGeometry decl_use
fine_structure_leakage in IndisputableMonolith.Physics.MixingGeometry decl_use
CKMElement in IndisputableMonolith.Physics.ThreeGenerations decl_use
no_fourth_generation in IndisputableMonolith.Physics.ThreeGenerations decl_use
chartOnQuotient_well_defined in IndisputableMonolith.RecogGeom.Charts decl_use
overlap_le_one in IndisputableMonolith.YM.Dobrushin decl_use
overlap_nonneg in IndisputableMonolith.YM.Dobrushin decl_use
row in IndisputableMonolith.YM.Dobrushin decl_use
TransferOperator in IndisputableMonolith.YM.OS decl_use

Lean names referenced from this declaration's body.