Lemma A.3 - Frozen features off the training span
ProvedFeatureDistortion.FrozenOrthogonalFeaturesNotation: , is the input dimension, the feature dimension, the data map, the labels, the features, and the head. Adjoint means Euclidean transpose. The loss is , with no normalization. The probability model, when present, is explicitly specified below; deterministic flow statements involve no random data assumption.
For every triple of natural numbers , every continuous real-linear map , every , every , every continuous real-linear map , and every pair of functions and , assume , , and that for every real derivatives within exist with values and , the latter being a derivative in the space of continuous linear maps. Then for every real and every orthogonal to every vector with , one has . Thus the conclusion uses the orthogonal complement of . Adjoints and orthogonality are Euclidean. All dimensions may be zero; if this orthogonal complement is only is tested, and if every is tested. Existence of such curves and conditions at negative times are not asserted.
Formalization note: Direct source invariant, valid for arbitrary labels. Source: Kumar, Raghunathan, Jones, Ma, and Liang, Fine-Tuning can Distort Pretrained Features and Underperform Out-of-Distribution, ICLR 2022, https://arxiv.org/pdf/2202.10054v1. Appendix A.2, PDF p. 24, Lemma A.3, equations (A.15)--(A.18). Source-backed parent: Section 3.4, PDF p. 10, Proposition 3.7, equations (3.10)--(3.11); Appendix A.7, PDF pp. 45--47.
import Definitions.Def_FeatureDistortion_Model open MeasureTheory Filter open scoped Topology
namespace FeatureDistortion
theorem FrozenOrthogonalFeatures :
∀ (n d k : ℕ) (X : Vec d →L[ℝ] Vec n) (Y : Vec n)
(v₀ : Vec k) (B₀ : Features d k) (γ : Trajectory d k),
IsFineTuningFlow X Y v₀ B₀ γ →
∀ (t : ℝ), 0 ≤ t → ∀ x ∈ (rowSpace X)ᗮ, γ.features t x = B₀ x := by sorry
end FeatureDistortion
Read-back
What the Lean code literally says, in plain math · gpt-6
For every triple of natural numbers , every continuous real-linear map , every , every , every continuous real-linear map , and every pair of functions and , assume , , and that for every real derivatives within exist with values and , the latter being a derivative in the space of continuous linear maps. Then for every real and every orthogonal to every vector with , one has . Thus the conclusion uses the orthogonal complement of . Adjoints and orthogonality are Euclidean. All dimensions may be zero; if this orthogonal complement is only is tested, and if every is tested. Existence of such curves and conditions at negative times are not asserted.
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.