OAI/Analysis/LipschitzHilbert/Trees/SourceBlockDisintegration.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Distribute each true child amount among its original top weights. This is the finite transition identity used to attach one terminal path to each top, including tops that stop inside a source block.

  1. theorem OAI.LipschitzHilbert.AngularGrid.sourceBlock_disintegrate_children line 15
  2. theorem OAI.LipschitzHilbert.AngularGrid.sourceBlock_disintegrate_denominator line 57