OAI/MeasureTheory/Falconer/Recursion/ProfileLoss.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Ambient-dimensional losses in the scalar branch ledger

The policy parameter remains sigma. Only the numerical loss parameter is enlarged, so the branch schedule and its retained descriptor lists do not change.

  1. def OAI.Falconer.profileLossParameter line 14
  2. theorem OAI.Falconer.profileLossParameter_nonneg line 17
  3. theorem OAI.Falconer.profile_graph_loss_le line 22
  4. theorem OAI.Falconer.profile_source_branch_exponent line 30