OAI/Analysis/LipschitzHilbert/Packets/SourceFrozenDensitySum.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Finite integration of the original frozen long-tree expression over its common density masks. The exponents and cell volumes are exact.

  1. theorem OAI.LipschitzHilbert.SourceLabeledLattice.finite_frozen_density_integral line 18