OAI/Analysis/LipschitzHilbert/Trees/SourceLpDamping.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Constant scalar damping acts exactly on the Lp root. The vertex estimate on the prescribed imaginary ball therefore extends to the whole tube using the manuscript's Gaussian tail estimate.

  1. theorem OAI.LipschitzHilbert.source_lp_root_smul line 16
  2. theorem OAI.LipschitzHilbert.source_lp_power_smul_integrable line 26
  3. theorem OAI.LipschitzHilbert.eventually_source_damped_vertex_root line 32