OAI/Analysis/LipschitzHilbert/Trees/SourcePathValues.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LipschitzHilbert.diagonalModulation_real_smul line 14
2. theorem OAI.LipschitzHilbert.source_snapshot_value_as_prediction line 19
3. theorem OAI.LipschitzHilbert.source_prediction_path_value line 27

   Source documentation

   The source actual ratio in any common unitary path frame.

   theorem source_prediction_path_value {n p μ : ℝ} (hn : 0 < n) (hp : 0 < p)
       (c : ι → ℝ) (hc : ∀ i, 0 < c i) (A : ι → EuclideanSpace ℂ κ) (lam : ι → ℂ)
       (i₀ : ι) (hlam : lam i₀ ≠ 0) (U : EuclideanSpace ℂ κ →ₗᵢ[ℂ] EuclideanSpace ℂ κ) :
       sourcePredictionValue p μ n c A lam =
         energyRatio p
           (1+‖(c i₀/n)^(1/p) • U ((c i₀)^(μ-1) • A i₀)‖^p+
             ∑ i : RemainderIndex i₀, (c i/n)*‖(c i)^(μ-1) • A i‖^p)
           (((c i₀/n)^(1-μ-1/p)*‖lam i₀‖) •
             ((c i₀/n)^(1/p) • U ((c i₀)^(μ-1) • A i₀))+
             (scalarPhase (lam i₀))⁻¹ • U
               (∑ i : RemainderIndex i₀, ((n^(μ-1):ℝ):ℂ) • (lam i • A i))) := by
   …

   Mentions: OAI.LipschitzHilbert.sourcePredictionValue, OAI.LipschitzHilbert.energyRatio, OAI.LipschitzHilbert.scalarPhase

4. theorem OAI.LipschitzHilbert.source_snapshot_path_value line 47

   Source documentation

   The model leaves precisely the distinguished path unshrunk.

   theorem source_snapshot_path_value {n p μ ε : ℝ} (hn : 0 < n) (hp : 0 < p)
       (c : ι → ℝ) (hc : ∀ i, 0 < c i) (A : ι → EuclideanSpace ℂ κ) (lam : ι → ℂ)
       (i₀ : ι) (hlam : lam i₀ ≠ 0) (f : ι → κ → ℝ) (b : ℝ) :
       let shrink := fun i => if i = i₀ then A i else radialShrink (2*ε*c i) (A i)
   …

   Mentions: OAI.LipschitzHilbert.radialShrink