OAI/Analysis/LipschitzHilbert/Trees/SourceRadialIntegral.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The literal radial logarithmic loss has integral O(epsilon), uniformly in the number of eligible levels. This is the scalar integral used by the common-translation boundary average.

  1. theorem OAI.LipschitzHilbert.AngularGrid.nearbyEligibleMass_measurable_radius line 16
  2. theorem OAI.LipschitzHilbert.AngularGrid.radial_log_ratio_integral_le line 29