OAI/Analysis/PathSelection/CompactProfiles.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Compact analytic profiles and parameter-dependent contour integrals.

  1. def OAI.DegeneratingTrees.radialClip line 18
  2. theorem OAI.DegeneratingTrees.continuous_radialClip line 20
  3. theorem OAI.DegeneratingTrees.norm_radialClip_le line 25
  4. theorem OAI.DegeneratingTrees.radialClip_eq line 31
  5. theorem OAI.DegeneratingTrees.localized_profile line 37
  6. theorem OAI.DegeneratingTrees.analytic_compact_profile line 82
  7. def OAI.DegeneratingTrees.compactProfile line 136
  8. theorem OAI.DegeneratingTrees.compactProfile_apply line 141
  9. theorem OAI.DegeneratingTrees.analytic_compactProfile line 146
  10. theorem OAI.DegeneratingTrees.analytic_circleIntegral line 164
  11. theorem OAI.DegeneratingTrees.analytic_contourMoment_general line 187