OAI/Analysis/LipschitzHilbert/Trees/SourceInsignificantShrink.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Insignificant children are removed by the same radial shrink used in the denominator comparison. There is no extra exceptional-child premise.

  1. theorem OAI.LipschitzHilbert.eventually_source_insignificant_error line 14
  2. theorem OAI.LipschitzHilbert.eventually_source_insignificant_shrink line 45

    Source documentation

    A nonsignificant amplitude is zero in the graph snapshot, with the same shrink radius that controls every displaced denominator.

    theorem eventually_source_insignificant_shrink (Q : ℝ) :
    ∀ᶠ L : ℝ in atTop, ∀ (E : Type) [NormedAddCommGroup E] [NormedSpace ℝ E]
      (c : ℝ) (A : E), 0 ≤ c →
      ‖A‖ ≤ (L^Q*Real.exp (-L*Real.log L))*c →
      radialShrink (2*SourceParameters.step L^(-(1/8:ℝ))*c) A = 0 := by
…

    Mentions: OAI.LipschitzHilbert.radialShrink, OAI.LipschitzHilbert.SourceParameters.step