OAI/Analysis/LipschitzHilbert/Packets/PacketDataDensityForestIntegral.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Integrate all trees in the actual sharp density forest. Coefficients are controlled by the original size tests, and the forest area is supplied by disjoint witnesses rather than by an additional analytic assumption.

  1. theorem OAI.LipschitzHilbert.PacketLatticeData.exists_density_forest_integral line 16