OAI/Analysis/LipschitzHilbert/Trees/SourceMaskedFrozenEstimate.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Frozen integration for the actual masks supplied by a reference coordinate change. No grid assumption is needed after the mass bound.

  1. theorem OAI.LipschitzHilbert.SourceLabeledLattice.exists_masked_frozen_tree_estimate line 14