SourcePredictionShrink.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The source snapshot shrinkage gives the one-sided denominator comparison and preserves numerator motion with its child-mass factor.

theorem OAI.LipschitzHilbert.prediction_mass_scale_factor line 12

theorem OAI.LipschitzHilbert.source_prediction_denominator_shrink line 23

Source documentation

Apply the source shrinkage to the original amplitude, before mass normalization. The resulting model denominator is below every moved one.

theorem source_prediction_denominator_shrink {n n' c c' p μ ε : ℝ}
    (hn : 0 < n) (hn' : 0 < n') (hc : 0 < c) (hc' : 0 < c')
    (hp : 0 < p) (hε : 0 ≤ ε) (U : E →ₗᵢ[ℝ] E) (A A' : E)
    (hmotion : ‖massPowerScale n' c' (-(1/p)) (μ-1+1/p) • A'-
        U (massPowerScale n c (-(1/p)) (μ-1+1/p) • A)‖ ≤
      ε*(c/n)^(1/p)*c^μ) :
    (c/n)*‖c^(μ-1) • radialShrink (2*ε*c) A‖^p ≤
      (c'/n')*‖c'^(μ-1) • A'‖^p := by
…

Mentions: OAI.LipschitzHilbert.massPowerScale, OAI.LipschitzHilbert.radialShrink

theorem OAI.LipschitzHilbert.source_prediction_shrink_zero line 60

theorem OAI.LipschitzHilbert.source_prediction_shrunk_numerator line 72

Source documentation

Shrinking the snapshot costs another two copies of the same relative-child-mass error. The common diagonal carrier stays explicit.

theorem source_prediction_shrunk_numerator {n c μ ε K : ℝ}
    (hn : 0 < n) (hc : 0 ≤ c) (hε : 0 ≤ ε) (hK : n^μ ≤ K)
    (U : E →ₗᵢ[ℂ] E) (A actual : E) (lam : ℂ) (hlam : ‖lam‖ ≤ 1)
    (hmotion : ‖actual-((n^(μ-1):ℝ):ℂ) • (lam • U A)‖ ≤ ε*K*(c/n)) :
    ‖actual-((n^(μ-1):ℝ):ℂ) •
      (lam • U (radialShrink (2*ε*c) A))‖ ≤ (3*ε*K)*(c/n) := by
…

Mentions: OAI.LipschitzHilbert.radialShrink