OAI/Analysis/LipschitzHilbert/Trees/SourceDensityTail.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The density kernel has a quantitative tail outside a dilated slope box. This turns a weighted density test into the unweighted witness used by the finite keeper construction.

  1. def OAI.LipschitzHilbert.SlopeBox.densityKernel line 15
  2. theorem OAI.LipschitzHilbert.SlopeBox.densityKernel_nonneg line 18
  3. theorem OAI.LipschitzHilbert.SlopeBox.densityKernel_le_one line 21
  4. theorem OAI.LipschitzHilbert.SlopeBox.densityKernel_eq_weight line 25
  5. theorem OAI.LipschitzHilbert.SlopeBox.densityKernel_integrable line 30
  6. theorem OAI.LipschitzHilbert.SlopeBox.integral_densityKernel line 35
  7. theorem OAI.LipschitzHilbert.densitySpatialBox_iff line 46
  8. theorem OAI.LipschitzHilbert.densitySpatialBox_radius_lt line 52
  9. theorem OAI.LipschitzHilbert.densityKernel_tail line 62
  10. theorem OAI.LipschitzHilbert.density_witness_mass line 89
  11. theorem OAI.LipschitzHilbert.density_tail_at_power_scale line 130

    Source documentation

    A fixed decay order gives the manuscript's small polynomial spatial enlargement at every polynomial density threshold.

    theorem density_tail_at_power_scale (a : ℝ) (ha : 0 ≤ a) :
    ∃ L0 : ℝ, 1 ≤ L0 ∧ ∀ L : ℝ, L0 ≤ L →
      (L^(a/100+1))^(3-(203:ℝ))*(∫ z, topProfile 3 z ∂volume.prod volume) ≤ L^(-a)/2 := by
…

    Mentions: OAI.LipschitzHilbert.topProfile