OAI/Analysis/LipschitzHilbert/Trees/SourceCommonTerminalIntegral.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Per-top path integrals are unchanged when their terminal counts are replaced by a common terminal count. The original good set, weights and physical packet values are preserved.

  1. theorem OAI.LipschitzHilbert.AngularGrid.sourceActivePathValue_integral_count_congr line 15
  2. theorem OAI.LipschitzHilbert.AngularGrid.sourceActivePathValue_common_terminal_integral line 49