OAI/Analysis/LipschitzHilbert/Trees/SourceBoundaryMajorant.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The source boundary log loss is bounded by the radial near-boundary majorant at its actual normalized distance. Far from boundaries it vanishes.

  1. theorem OAI.LipschitzHilbert.AngularGrid.source_boundary_log_loss_le_majorant line 14