OAI/Analysis/LipschitzHilbert/Trees/SourceTreeVertexIntegral.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Integrating the actual finite packet-tree vertex bound. The only path inputs are the restricted good-path integrals, which are supplied by the marked line and plane estimates.

  1. theorem OAI.LipschitzHilbert.AngularGrid.source_packet_vertex_integral line 16