Discovery.LinearDisentanglement.SimultaneousCongruence
Two results on recovering a unit-diagonal matrix B that makes B·Aₑ·Bᵀ diagonal for every environment e.
Definitions 14 core · 0 supporting This module defines the paper-independent objects used to deform a simultaneous congruence representation along an affine-collinear pair of diagonal shifts.
Two-coordinate deformations for collinear congruence families
This module defines the paper-independent objects used to deform a simultaneous congruence representation along an affine-collinear pair of diagonal shifts. The deformation first mixes the two selected rows and then rescales them so that a unit-diagonal normalization is retained.
structure AffineLineCertificate reviewed
⚑ flagged
Causalean.Discovery.LinearDisentanglement.SimultaneousCongruence
A concrete certificate that the selected two-coordinate shift cloud is contained in the affine line u x + v y = c, with a nonzero normal vector.
Definition (Lean source)
parameters
fields
First component of the line's normal vector.
u :
ℝ
Second component of the line's normal vector.
v :
ℝ
Affine offset of the line.
c :
ℝ
The normal vector is nonzero.
normal_ne :
u ≠ 0 ∨ v ≠ 0
Every selected shift pair lies on the certified affine line.
equation :
∀ e, u * s e i + v * s e j = c
def pairShear reviewed
⚑ flagged
Causalean.Discovery.LinearDisentanglement.SimultaneousCongruence
The elementary two-row shear traces the observationally ambiguous direction associated with selected coordinates i,j, line normal u,v and deformation t in dimension d. It perturbs only the selected pair, or their common diagonal if they coincide.
def firstNormalizationDenom reviewed
⚑ flagged
Causalean.Discovery.LinearDisentanglement.SimultaneousCongruence
The first normalization denominator is the row-scale correction that keeps the first selected diagonal entry fixed after shearing reference matrix B at coordinates i,j, with coefficient v and magnitude t in dimension d.
def secondNormalizationDenom reviewed
⚑ flagged
Causalean.Discovery.LinearDisentanglement.SimultaneousCongruence
The second normalization denominator is the row-scale correction that keeps the second selected diagonal entry fixed after shearing reference matrix B at coordinates i,j, with coefficient u and magnitude t in dimension d.
def pairRowNormalizer reviewed
⚑ flagged
Causalean.Discovery.LinearDisentanglement.SimultaneousCongruence
The pair row normalizer compensates row scaling after deforming selected coordinates i,j of reference matrix B, using line normal u,v and magnitude t in dimension d. It rescales only the selected rows; zero denominators use the library's zero reciprocal convention.
Definition (Lean source)
parameters
def
given by
diagonal fun k ↦ if k
= i then (firstNormalizationDenom B i j v t)⁻¹ else if k = j then (secondNormalizationDenom B i j u t)⁻¹ else 1
def normalizedPairDeformation reviewed
⚑ flagged
Causalean.Discovery.LinearDisentanglement.SimultaneousCongruence
The normalized two-coordinate deformation combines a shear with row rescaling, moving along the ambiguity generated by coordinates i,j and line normal u,v at magnitude t for reference matrix B in dimension d.
Definition (Lean source)
def deformedDiagonalizer reviewed
⚑ flagged
Causalean.Discovery.LinearDisentanglement.SimultaneousCongruence
The deformed diagonalizer applies the normalized ambiguity direction to reference diagonalizer B, mixing coordinates i,j according to line normal u,v and magnitude t in dimension d.
Definition (Lean source)
def PairCycleAdmissible reviewed
⚑ flagged
Causalean.Discovery.LinearDisentanglement.SimultaneousCongruence
Pair-cycle admissibility rules out the singular two-coordinate feedback cycle in matrix B: the opposite entries at coordinates i,j must not multiply to one in dimension d.
def commonShiftCrossTerm reviewed
⚑ flagged
Causalean.Discovery.LinearDisentanglement.SimultaneousCongruence
The common shift cross term is the off-diagonal contribution shared by all environments after deforming reference matrix B at coordinates i,j, determined by line normal, offset, and magnitude u,v,c,t in dimension d.
Definition (Lean source)
parameters
def
commonShiftCrossTerm B i j u v c t :
ℝ
given by
(firstNormalizationDenom B i j v t)⁻¹ * (secondNormalizationDenom B i j u t)⁻¹ * (t * c)
def pairSymmetricOffDiagonal reviewed
⚑ flagged
Causalean.Discovery.LinearDisentanglement.SimultaneousCongruence
The symmetric selected-pair matrix places value x in both orientations of coordinates i,j in dimension d, isolating the common cross term created by a pair deformation.
def deformedInvariant reviewed
⚑ flagged
Causalean.Discovery.LinearDisentanglement.SimultaneousCongruence
The deformed invariant matrix absorbs the environment-independent cross term so the represented covariance family can remain unchanged. From reference diagonalizer and invariant matrix, selected coordinates, and line data and magnitude in dimension d, it first forms the normalized pair deformation, then transforms the invariant and adds the common symmetric term.
Definition (Lean source)
parameters
def
given by
T :
normalizedPairDeformation B i j u v t
T * Ω * T.transpose + pairSymmetricOffDiagonal i j (commonShiftCrossTerm B i j u v c t)
def deformedShift reviewed
⚑ flagged
Causalean.Discovery.LinearDisentanglement.SimultaneousCongruence
The deformed shift records the new environment-specific diagonal after transforming original shift s through reference diagonalizer B at coordinates i,j, with line normal u,v and magnitude t in dimension d; it first forms the normalized pair deformation.
def representedCovariance reviewed
⚑ flagged
Causalean.Discovery.LinearDisentanglement.SimultaneousCongruence
The represented covariance matrix maps an invariant and diagonalizer plus an environment-specific diagonal shift back to observed coordinates in dimension d. An invertible diagonalizer is required for the intended interpretation; the library's singular inverse convention returns zero otherwise.
def RepresentsCovarianceFamily reviewed
⚑ flagged
Causalean.Discovery.LinearDisentanglement.SimultaneousCongruence
A covariance family is represented when every environment in E shares diagonalizer B and invariant component Ω while varying only through shift family s, reproducing covariances Sigma in dimension d. Invertibility is deliberately separate; a singular diagonalizer represents only the zero family.
Definition (Lean source)
parameters
def
RepresentsCovarianceFamily Sigma B Ω s :
Prop
given by
Sigma e = representedCovariance B Ω (s e)
DefinitionsPairwiseAffine 17 core · 7 supporting This module defines pair-dependent affine-minor separation, off-diagonal approximate simultaneous congruence, the entrywise Euclidean matrix norm used for aggregation, and the explicit constants and scale envelopes used ★ opNorm_le_conditionRoot
Pairwise-affine simultaneous-congruence stability: definitions
This module defines pair-dependent affine-minor separation, off-diagonal approximate simultaneous congruence, the entrywise Euclidean matrix norm used for aggregation, and the explicit constants and scale envelopes used by the local stability theorem.
Unlike AffineMinorSeparated, the separation predicate here does not select one common
base and a full-dimensional minor. Its three witnessing environments may depend on the
coordinate pair.
def pairAffineDet reviewed
⚑ flagged
Causalean.Discovery.LinearDisentanglement.SimultaneousCongruence
The pairwise affine determinant measures whether three environmental shifts span area in coordinates i,j, using shift family s and environments e₀,e₁,e₂ from collection E in dimension p.
def PairwiseAffineSeparated reviewed
⚑ flagged
Causalean.Discovery.LinearDisentanglement.SimultaneousCongruence
Pairwise affine separation ensures every coordinate pair receives enough independent environmental movement to be distinguished: shift family s over finite environments E has a three-environment area of at least margin δ for every pair in dimension p.
Definition (Lean source)
parameters
def
PairwiseAffineSeparated s δ :
Prop
given by
∃ e₀ e₁ e₂ : E, δ ≤ |pairAffineDet s i j e₀ e₁ e₂|
def OffDiagonalApproximateCongruence reviewed
⚑ flagged
Causalean.Discovery.LinearDisentanglement.SimultaneousCongruence
Off-diagonal approximate congruence accepts candidate coordinates B when all cross-coordinate terms of observed matrices A stay below tolerance ε, over finite environments E in dimension p.
def transitionError reviewed
⚑ flagged
Causalean.Discovery.LinearDisentanglement.SimultaneousCongruence
The transition error directly measures departure from exact recovery by comparing candidate coordinates with reference coordinates in dimension p.
Definition (Lean source)
def entryL2 reviewed
⚑ flagged
Causalean.Discovery.LinearDisentanglement.SimultaneousCongruence
The entrywise Euclidean size aggregates all coordinate errors of matrix R in dimension p, using its Frobenius norm.
def pairwiseSolveFactor reviewed
⚑ flagged
Causalean.Discovery.LinearDisentanglement.SimultaneousCongruence
The pairwise solve factor converts off-diagonal residuals into coordinate-pair error; it grows with shift scale M and shrinks with separation margin δ.
Definition (Lean source)
parameters
M δ :
ℝ
def
pairwiseSolveFactor M δ :
ℝ
given by
6 * M / δ
def pairwiseAggregateFactor reviewed
⚑ flagged
Causalean.Discovery.LinearDisentanglement.SimultaneousCongruence
The pairwise aggregate factor combines all ordered coordinate-pair errors under dimension p, shift scale M, separation margin δ, and matrix scale L.
Definition (Lean source)
parameters
p :
ℕ
M δ L :
ℝ
def
pairwiseAggregateFactor p M δ L :
ℝ
given by
pairwiseSolveFactor M δ * sqrt ((p : ℝ) * (p - 1 : ℕ) * (1 + L ^ 2))
def pairwiseStabilityConstant reviewed
⚑ flagged
Causalean.Discovery.LinearDisentanglement.SimultaneousCongruence
The pairwise stability constant turns residual size into diagonalizer error under dimension p, shift scale M, separation margin δ, and matrix scale L.
Definition (Lean source)
parameters
p :
ℕ
M δ L :
ℝ
def
pairwiseStabilityConstant p M δ L :
ℝ
given by
16 * pairwiseAggregateFactor p M δ L * L ^ 3
def pairwiseResidualRadius reviewed
⚑ flagged
Causalean.Discovery.LinearDisentanglement.SimultaneousCongruence
The pairwise residual radius sets the noise threshold used to enter the identity branch, determined by dimension p, shift scale M, separation margin δ, and matrix scale L.
Definition (Lean source)
parameters
p :
ℕ
M δ L :
ℝ
def
pairwiseResidualRadius p M δ L :
ℝ
given by
1 / (32 * (max 1 (pairwiseAggregateFactor p M δ L)) ^ 2 * M)
def pairwiseLocalRadius reviewed
⚑ flagged
Causalean.Discovery.LinearDisentanglement.SimultaneousCongruence
The pairwise local radius sets the reference-neighborhood size used to force a candidate onto the identity branch, determined by dimension p, shift scale M, separation margin δ, matrix scale L, and inverse-norm envelope J.
Definition (Lean source)
parameters
p :
ℕ
M δ L J :
ℝ
def
pairwiseLocalRadius p M δ L J :
ℝ
given by
def conditionRoot reviewed
⚑ flagged
Causalean.Discovery.LinearDisentanglement.SimultaneousCongruence
The condition root is the scale used to convert determinant and condition information operator-norm bound in dimension p under condition envelope κ. At dimension zero the exponent conventions make the value one.
Definition (Lean source)
parameters
p :
ℕ
κ :
ℝ
def
conditionRoot p κ :
ℝ
given by
((Nat.factorial p : ℝ) * κ ^ (p - 1)) ^ (1 / (p : ℝ))
abbrev PairMatrixNormBound reviewed
⚑ flagged
Causalean.Discovery.LinearDisentanglement.SimultaneousCongruence
The pair matrix-norm bound keeps reference and candidate matrices within scale L in dimension p; it is the canonical pair matrix-scale condition under a compatibility name.
Definition (Lean source)
def InReferenceNeighborhood reviewed
⚑ flagged
Causalean.Discovery.LinearDisentanglement.SimultaneousCongruence
Membership in the reference neighborhood requires candidate and reference matrices to differ by at most entrywise radius ρ in dimension p.
def DetConditionEnvelope reviewed
⚑ flagged
Causalean.Discovery.LinearDisentanglement.SimultaneousCongruence
The determinant-condition envelope rules out unstable matrices B in dimension p by requiring (1) nonsingularity, (2) a factorial determinant cap, and (3) condition number at most envelope κ for that envelope.
Definition (Lean source)
parameters
def
DetConditionEnvelope κ B :
Prop
given by
clause 1
IsUnit B.det
clause 2
|B.det| ≤ (Nat.factorial p : ℝ)
clause 3
operatorConditionNumber B ≤ κ
def PairDetConditionEnvelope reviewed
⚑ flagged
Causalean.Discovery.LinearDisentanglement.SimultaneousCongruence
The pair determinant-condition envelope places reference and candidate matrices in the same stable class in dimension p: (1) the reference meets the envelope and (2) the candidate meets it, for condition limit κ.
Definition (Lean source)
parameters
def
PairDetConditionEnvelope κ B₀ B :
Prop
def InIdentityBranch reviewed
⚑ flagged
Causalean.Discovery.LinearDisentanglement.SimultaneousCongruence
Membership in the identity branch rules out large relabeling or sign ambiguities for reference and candidate matrices in dimension p, under shift scale, separation, and matrix scale: (1) transition error is at most one, and (2) its amplified pairwise error is at most one half.
Definition (Lean source)
parameters
def
InIdentityBranch M δ L B₀ B :
Prop
theorem opNorm_le_conditionRoot reviewed
⚑ flagged
Causalean.Discovery.LinearDisentanglement.SimultaneousCongruence
The determinant-condition root bounds the matrix operator norm, turning matrix B's determinant-condition certificate into a scale bound in dimension p for condition envelope κ, when the dimension is positive.
Formal statement
hypotheses
conclusion
‖B‖ ≤ conditionRoot p κ
Proof (Lean source)
-- Proof route: order the singular values;
-- `cond(B) ≤ κ` bounds every lower singular value below by `‖B‖/κ`, while their
-- product is `|det B| ≤ p!`. Take the positive `p`-th root.
theorem opNorm_le_conditionRoot {p : ℕ} {κ : ℝ} (B : SqMatrix p)
(hp : 0 < p)
(henv : DetConditionEnvelope κ B) :
‖B‖ ≤ conditionRoot p κ := by
have hcond_nonneg : 0 ≤ operatorConditionNumber B :=
mul_nonneg (norm_nonneg B) (norm_nonneg B⁻¹)
have hpow : ‖B‖ ^ p ≤ (Nat.factorial p : ℝ) * κ ^ (p - 1) := by
calc
‖B‖ ^ p ≤ |B.det| * operatorConditionNumber B ^ (p - 1) :=
opNorm_pow_le_det_mul_condition_pow hp B henv.1
_ ≤ (Nat.factorial p : ℝ) * κ ^ (p - 1) := by
exact mul_le_mul henv.2.1
(pow_le_pow_left₀ hcond_nonneg henv.2.2 _)
(pow_nonneg hcond_nonneg _) (by positivity)
unfold conditionRoot
have hrpow := Real.rpow_le_rpow (pow_nonneg (norm_nonneg B) _) hpow
(show 0 ≤ 1 / (p : ℝ) by positivity)
calc
‖B‖ = (‖B‖ ^ p) ^ (1 / (p : ℝ)) := by
rw [← Real.rpow_natCast]
rw [← Real.rpow_mul (norm_nonneg B)]
have hpR : (p : ℝ) ≠ 0 := by positivity
rw [mul_div_cancel₀ 1 hpR, Real.rpow_one]
_ ≤ ((Nat.factorial p : ℝ) * κ ^ (p - 1)) ^ (1 / (p : ℝ)) := hrpow
7 supporting declarations (lemmas, instances)
-
entryL2_eq_frobenius_normtheorem — The entrywise Euclidean size is exactly the Frobenius norm for matrix R in dimension p, allowing standard matrix-norm results to apply directly.hypothesesp :ℕR :SqMatrix p -
entryL2_eq_sqrttheorem — Entrywise Euclidean size is the root-sum-of-squares of all entries for matrix R in dimension p.Proof (Lean source)
theorem entryL2_eq_sqrt {p : ℕ} (R : SqMatrix p) : entryL2 R = sqrt (∑ i, ∑ j, |R i j| ^ 2) := by rw [entryL2, Matrix.frobenius_norm_def, Real.sqrt_eq_rpow] simp only [Real.rpow_two, Real.norm_eq_abs] -
entryL2_nonnegtheorem — Entrywise Euclidean size cannot be negative for matrix R in dimension p, as required for radius and error bounds.Proof (Lean source)
theorem entryL2_nonneg {p : ℕ} (R : SqMatrix p) : 0 ≤ entryL2 R := by rw [entryL2_eq_sqrt] exact Real.sqrt_nonneg _ -
pairwiseResidualRadius_postheorem — The explicit pairwise residual threshold is strictly positive when shift scale M is positive, for any separation margin δ and matrix scale L in dimension p.Proof (Lean source)
theorem pairwiseResidualRadius_pos {p : ℕ} {M δ L : ℝ} (hM : 0 < M) : 0 < pairwiseResidualRadius p M δ L := by unfold pairwiseResidualRadius positivity -
pairwiseLocalRadius_postheorem — The explicit local reference-neighborhood radius is strictly positive when dimension p, shift scale M, and inverse envelope J are positive, for any separation margin δ and matrix scale L.hypothesesp :ℕM δ L J :ℝhp :0 < phM :0 < MhJ :0 < Jconclusion0 < pairwiseLocalRadius p M δ L JProof (Lean source)
theorem pairwiseLocalRadius_pos {p : ℕ} {M δ L J : ℝ} (hp : 0 < p) (hM : 0 < M) (hJ : 0 < J) : 0 < pairwiseLocalRadius p M δ L J := by unfold pairwiseLocalRadius positivity -
one_le_conditionRoottheorem — The determinant-condition root is at least one in dimension p under condition envelope κ, provided the dimension is positive and the envelope is at least one.Proof (Lean source)
theorem one_le_conditionRoot {p : ℕ} {κ : ℝ} (hp : 0 < p) (hκ : 1 ≤ κ) : 1 ≤ conditionRoot p κ := by unfold conditionRoot apply Real.one_le_rpow · have hf : (1 : ℝ) ≤ factorial p := by exact_mod_cast Nat.factorial_pos p have hk : (1 : ℝ) ≤ κ ^ (p - 1) := one_le_pow₀ hκ nlinarith · positivity -
pairMatrixNormBound_conditionRoottheorem — One determinant-condition certificate yields a common operator-norm bound for both matrices, for reference and candidate B₀,B in dimension p under condition envelope κ, assuming positive dimension, envelope at least one, and the shared certificate.hypothesesconclusionPairMatrixNormBound (conditionRoot p κ) B₀ BProof (Lean source)
theorem pairMatrixNormBound_conditionRoot {p : ℕ} {κ : ℝ} (B₀ B : SqMatrix p) (hp : 0 < p) (hκ : 1 ≤ κ) (henv : PairDetConditionEnvelope κ B₀ B) : PairMatrixNormBound (conditionRoot p κ) B₀ B := by exact ⟨opNorm_le_conditionRoot B₀ hp henv.1, opNorm_le_conditionRoot B hp henv.2⟩
Algebra 1 core · 19 supporting This module records the entry formulas, invertibility and normalization facts, cycle product identity, shift nonnegativity, and exact congruence decomposition for the two-coordinate construction. ★ representedCovariance_deformation_eq
Algebra of the normalized two-coordinate deformation
This module records the entry formulas, invertibility and normalization facts, cycle product identity, shift nonnegativity, and exact congruence decomposition for the two-coordinate construction.
theorem representedCovariance_deformation_eq reviewed
⚑ flagged
Causalean.Discovery.LinearDisentanglement.SimultaneousCongruence
The explicit pair deformation leaves every represented covariance unchanged, proving observational equivalence for diagonalizer B, invariant Ω, shifts s, certificate cert, parameter t, and environment e over environment type E in dimension d, when coordinates i,j are distinct and the normalized deformation is invertible.
Formal statement
hypotheses
d :
ℕ
E :
Type*
B Ω :
SqMatrix d
i j :
Fin d
hij :
i ≠ j
s :
E → Fin d → ℝ
cert :
AffineLineCertificate s i j
t :
ℝ
e :
E
hT :
IsUnit (normalizedPairDeformation B i j cert.u cert.v t).det
conclusion
representedCovariance (deformedDiagonalizer B i j cert.u cert.v t) (deformedInvariant B Ω i j cert.u cert.v cert.c t) (deformedShift B i j cert.u cert.v t (s e))
= representedCovariance B Ω (s e)
Proof (Lean source)
theorem representedCovariance_deformation_eq {d : ℕ} {E : Type*}
(B Ω : SqMatrix d) {i j : Fin d} (hij : i ≠ j) (s : E → Fin d → ℝ)
(cert : AffineLineCertificate s i j) (t : ℝ) (e : E)
(hT : IsUnit (normalizedPairDeformation B i j cert.u cert.v t).det) :
representedCovariance
(deformedDiagonalizer B i j cert.u cert.v t)
(deformedInvariant B Ω i j cert.u cert.v cert.c t)
(deformedShift B i j cert.u cert.v t (s e)) =
representedCovariance B Ω (s e) := by
let T := normalizedPairDeformation B i j cert.u cert.v t
have hTtr : IsUnit T.transpose.det := Matrix.isUnit_det_transpose T hT
unfold representedCovariance deformedDiagonalizer
change (T * B)⁻¹ *
(deformedInvariant B Ω i j cert.u cert.v cert.c t +
diagonal (deformedShift B i j cert.u cert.v t (s e))) *
((T * B)⁻¹).transpose = _
rw [← total_congruence_decomposition B Ω hij s cert t e]
rw [Matrix.mul_inv_rev, Matrix.transpose_mul, Matrix.transpose_nonsing_inv]
calc
(B⁻¹ * T⁻¹) * (T * (Ω + diagonal (s e)) * T.transpose) *
((T.transpose)⁻¹ * (B⁻¹).transpose) =
B⁻¹ * (T⁻¹ * T) * (Ω + diagonal (s e)) *
(T.transpose * (T.transpose)⁻¹) * (B⁻¹).transpose := by
noncomm_ring
_ = B⁻¹ * (Ω + diagonal (s e)) * (B⁻¹).transpose := by
rw [Matrix.nonsing_inv_mul T hT, Matrix.mul_nonsing_inv T.transpose hTtr]
simp
19 supporting declarations (lemmas, instances)
-
normalizedPairDeformation_zerotheorem — At zero deformation parameter, the normalized pair deformation is the identity matrix.hypothesesconclusionnormalizedPairDeformation B i j u v 0 = 1Proof (Lean source)
@[simp] theorem normalizedPairDeformation_zero {d : ℕ} (B : SqMatrix d) (i j : Fin d) (u v : ℝ) : normalizedPairDeformation B i j u v 0 = 1 := by classical have hR : pairRowNormalizer B i j u v 0 = 1 := by ext k l simp [pairRowNormalizer, firstNormalizationDenom, secondNormalizationDenom] have hS : pairShear i j u v 0 = 1 := by ext k l simp [pairShear] simp [normalizedPairDeformation, hR, hS] -
deformedDiagonalizer_zerotheorem — At zero deformation parameter, the deformed diagonalizer equals the reference diagonalizer.Proof (Lean source)
@[simp] theorem deformedDiagonalizer_zero {d : ℕ} (B : SqMatrix d) (i j : Fin d) (u v : ℝ) : deformedDiagonalizer B i j u v 0 = B := by simp [deformedDiagonalizer] -
deformedInvariant_zerotheorem — At zero deformation parameter, the transformed invariant is the original invariant matrix.hypothesesconclusiondeformedInvariant B Ω i j u v c 0 = ΩProof (Lean source)
@[simp] theorem deformedInvariant_zero {d : ℕ} (B Ω : SqMatrix d) (i j : Fin d) (u v c : ℝ) : deformedInvariant B Ω i j u v c 0 = Ω := by simp [deformedInvariant, commonShiftCrossTerm, pairSymmetricOffDiagonal] -
deformedShift_zerotheorem — At zero deformation parameter, the transformed diagonal shift is the original shift.hypothesesconclusiondeformedShift B i j u v 0 s = sProof (Lean source)
@[simp] theorem deformedShift_zero {d : ℕ} (B : SqMatrix d) (i j : Fin d) (u v : ℝ) (s : Fin d → ℝ) : deformedShift B i j u v 0 s = s := by funext k simp [deformedShift] -
pairShear_isUnit_dettheorem — When the selected coordinates are distinct and the selected shear-block determinant is nonzero, the elementary pair shear is invertible.hypothesesProof (Lean source)
theorem pairShear_isUnit_det {d : ℕ} {i j : Fin d} (hij : i ≠ j) {u v t : ℝ} (hdet : 1 - t ^ 2 * u * v ≠ 0) : IsUnit (pairShear i j u v t).det := by rw [pairShear_factorization hij, Matrix.det_mul, Matrix.det_mul] exact IsUnit.mul (IsUnit.mul (elementaryShear_isUnit_det hij.symm (t * u)) (diagonalReplace_isUnit_det j hdet)) (elementaryShear_isUnit_det hij (t * v)) -
pairRowNormalizer_isUnit_dettheorem — When both row-normalization denominators are nonzero, the diagonal row normalizer is invertible.hypothesesd :ℕB :SqMatrix di j :Fin du v t :ℝhfirst :firstNormalizationDenom B i j v t ≠ 0hsecond :secondNormalizationDenom B i j u t ≠ 0conclusionIsUnit (pairRowNormalizer B i j u v t).detProof (Lean source)
theorem pairRowNormalizer_isUnit_det {d : ℕ} (B : SqMatrix d) {i j : Fin d} {u v t : ℝ} (hfirst : firstNormalizationDenom B i j v t ≠ 0) (hsecond : secondNormalizationDenom B i j u t ≠ 0) : IsUnit (pairRowNormalizer B i j u v t).det := by rw [pairRowNormalizer, Matrix.det_diagonal, IsUnit.prod_iff] intro k hk split_ifs with hki hkj · exact (inv_ne_zero hfirst).isUnit · exact (inv_ne_zero hsecond).isUnit · exact isUnit_one -
normalizedPairDeformation_isUnit_dettheorem — When the selected coordinates are distinct, both normalization denominators are nonzero, and the shear determinant is nonzero, the normalized pair deformation is invertible.hypothesesd :ℕB :SqMatrix di j :Fin dhij :i ≠ ju v t :ℝhfirst :firstNormalizationDenom B i j v t ≠ 0hsecond :secondNormalizationDenom B i j u t ≠ 0hdet :1 - t ^ 2 * u * v ≠ 0conclusionIsUnit (normalizedPairDeformation B i j u v t).detProof (Lean source)
theorem normalizedPairDeformation_isUnit_det {d : ℕ} (B : SqMatrix d) {i j : Fin d} (hij : i ≠ j) {u v t : ℝ} (hfirst : firstNormalizationDenom B i j v t ≠ 0) (hsecond : secondNormalizationDenom B i j u t ≠ 0) (hdet : 1 - t ^ 2 * u * v ≠ 0) : IsUnit (normalizedPairDeformation B i j u v t).det := by rw [normalizedPairDeformation, Matrix.det_mul] exact IsUnit.mul (pairRowNormalizer_isUnit_det B hfirst hsecond) (pairShear_isUnit_det hij hdet) -
deformedDiagonalizer_unitDiagonaltheorem — When the selected coordinates are distinct, the reference diagonal is unit-normalized, and both normalization denominators are nonzero, row normalization restores unit diagonal.hypothesesd :ℕB :SqMatrix di j :Fin dhij :i ≠ jhB :u v t :ℝhfirst :firstNormalizationDenom B i j v t ≠ 0hsecond :secondNormalizationDenom B i j u t ≠ 0conclusionUnitDiagonal (deformedDiagonalizer B i j u v t)Proof (Lean source)
theorem deformedDiagonalizer_unitDiagonal {d : ℕ} (B : SqMatrix d) {i j : Fin d} (hij : i ≠ j) (hB : UnitDiagonal B) {u v t : ℝ} (hfirst : firstNormalizationDenom B i j v t ≠ 0) (hsecond : secondNormalizationDenom B i j u t ≠ 0) : UnitDiagonal (deformedDiagonalizer B i j u v t) := by intro k by_cases hki : k = i · subst k rw [deformedDiagonalizer_apply_first B hij, hB] change (firstNormalizationDenom B i j v t)⁻¹ * firstNormalizationDenom B i j v t = 1 exact inv_mul_cancel₀ hfirst · by_cases hkj : k = j · subst k rw [deformedDiagonalizer_apply_second B hij, hB] rw [show t * u * B i j + 1 = secondNormalizationDenom B i j u t by unfold secondNormalizationDenom ring] exact inv_mul_cancel₀ hsecond · rw [deformedDiagonalizer_apply_of_ne B hki hkj] exact hB k -
deformedDiagonalizer_cycle_identitytheorem — When the selected coordinates are distinct, the reference diagonal is unit-normalized, and both normalization denominators are nonzero, the selected cycle-product defect obeys the stated shear identity.hypothesesd :ℕB :SqMatrix di j :Fin dhij :i ≠ jhB :u v t :ℝhfirst :firstNormalizationDenom B i j v t ≠ 0hsecond :secondNormalizationDenom B i j u t ≠ 0conclusionfirstNormalizationDenom B i j v t * secondNormalizationDenom B i j u t * (deformedDiagonalizer B i j u v t i j * deformedDiagonalizer B i j u v t j i - 1)= (B i j * B j i - 1) * (1 - t ^ 2 * u * v)Proof (Lean source)
theorem deformedDiagonalizer_cycle_identity {d : ℕ} (B : SqMatrix d) {i j : Fin d} (hij : i ≠ j) (hB : UnitDiagonal B) {u v t : ℝ} (hfirst : firstNormalizationDenom B i j v t ≠ 0) (hsecond : secondNormalizationDenom B i j u t ≠ 0) : firstNormalizationDenom B i j v t * secondNormalizationDenom B i j u t * (deformedDiagonalizer B i j u v t i j * deformedDiagonalizer B i j u v t j i - 1) = (B i j * B j i - 1) * (1 - t ^ 2 * u * v) := by rw [deformedDiagonalizer_apply_first B hij, deformedDiagonalizer_apply_second B hij, hB, hB] unfold firstNormalizationDenom secondNormalizationDenom at * field_simp [hfirst, hsecond] ring -
deformedDiagonalizer_pairCycleAdmissibletheorem — When the selected coordinates are distinct, the reference diagonal is unit-normalized, its selected two-cycle is admissible, both normalization denominators are nonzero, and the shear determinant is nonzero, the deformed selected two-cycle remains admissible.hypothesesd :ℕB :SqMatrix di j :Fin dhij :i ≠ jhB :hcycle :PairCycleAdmissible B i ju v t :ℝhfirst :firstNormalizationDenom B i j v t ≠ 0hsecond :secondNormalizationDenom B i j u t ≠ 0hdet :1 - t ^ 2 * u * v ≠ 0conclusionPairCycleAdmissible (deformedDiagonalizer B i j u v t) i jProof (Lean source)
theorem deformedDiagonalizer_pairCycleAdmissible {d : ℕ} (B : SqMatrix d) {i j : Fin d} (hij : i ≠ j) (hB : UnitDiagonal B) (hcycle : PairCycleAdmissible B i j) {u v t : ℝ} (hfirst : firstNormalizationDenom B i j v t ≠ 0) (hsecond : secondNormalizationDenom B i j u t ≠ 0) (hdet : 1 - t ^ 2 * u * v ≠ 0) : PairCycleAdmissible (deformedDiagonalizer B i j u v t) i j := by intro hbad have h := deformedDiagonalizer_cycle_identity B hij hB hfirst hsecond rw [hbad, sub_self, mul_zero] at h have hright : (B i j * B j i - 1) * (1 - t ^ 2 * u * v) ≠ 0 := mul_ne_zero (sub_ne_zero.mpr hcycle) hdet exact hright h.symm -
deformedDiagonalizer_netheorem — When the selected coordinates are distinct, the reference diagonalizer is invertible, the line normal is nonzero, the deformation parameter is nonzero, and both normalization denominators are nonzero, the deformed diagonalizer differs from the reference.hypothesesd :ℕB :SqMatrix di j :Fin dhij :i ≠ jhBunit :IsUnit B.detu v t :ℝhnormal :u ≠ 0 ∨ v ≠ 0ht :t ≠ 0hfirst :firstNormalizationDenom B i j v t ≠ 0hsecond :secondNormalizationDenom B i j u t ≠ 0conclusiondeformedDiagonalizer B i j u v t ≠ BProof (Lean source)
theorem deformedDiagonalizer_ne {d : ℕ} (B : SqMatrix d) {i j : Fin d} (hij : i ≠ j) (hBunit : IsUnit B.det) {u v t : ℝ} (hnormal : u ≠ 0 ∨ v ≠ 0) (ht : t ≠ 0) (hfirst : firstNormalizationDenom B i j v t ≠ 0) (hsecond : secondNormalizationDenom B i j u t ≠ 0) : deformedDiagonalizer B i j u v t ≠ B := by intro heq have hmul : normalizedPairDeformation B i j u v t * B = B := heq have hT : normalizedPairDeformation B i j u v t = 1 := by calc normalizedPairDeformation B i j u v t = normalizedPairDeformation B i j u v t * (B * B⁻¹) := by rw [Matrix.mul_nonsing_inv B hBunit, Matrix.mul_one] _ = (normalizedPairDeformation B i j u v t * B) * B⁻¹ := by rw [Matrix.mul_assoc] _ = B * B⁻¹ := by rw [hmul] _ = 1 := Matrix.mul_nonsing_inv B hBunit rcases hnormal with hu | hv · have hentry := congrArg (fun M : SqMatrix d ↦ M j i) hT simp [normalizedPairDeformation_apply, hij, Ne.symm hij] at hentry rcases hentry with h | h | h · exact hsecond h · exact ht h · exact hu h · have hentry := congrArg (fun M : SqMatrix d ↦ M i j) hT simp [normalizedPairDeformation_apply, hij, Ne.symm hij] at hentry rcases hentry with h | h | h · exact hfirst h · exact ht h · exact hv h -
deformedShift_apply_firsttheorem — When the selected coordinates are distinct, the first transformed shift is its stated nonnegative weighted sum.hypothesesconclusiondeformedShift B i j u v t s i= (firstNormalizationDenom B i j v t)⁻¹ ^ 2 * (s i + t ^ 2 * v ^ 2 * s j)Proof (Lean source)
theorem deformedShift_apply_first {d : ℕ} (B : SqMatrix d) {i j : Fin d} (hij : i ≠ j) (u v t : ℝ) (s : Fin d → ℝ) : deformedShift B i j u v t s i = (firstNormalizationDenom B i j v t)⁻¹ ^ 2 * (s i + t ^ 2 * v ^ 2 * s j) := by classical rw [deformedShift_sum_squares] simp only [normalizedPairDeformation_apply] simp only [if_pos, Ne.symm hij, false_and, if_false, true_and] calc _ = ∑ l, ((if i = l then (firstNormalizationDenom B i j v t)⁻¹ ^ 2 * s l else 0) + (if j = l then (firstNormalizationDenom B i j v t)⁻¹ ^ 2 * (t ^ 2 * v ^ 2) * s l else 0)) := by apply Finset.sum_congr rfl intro l hl by_cases hil : i = l · by_cases hjl : j = l · exact (hij (hil.trans hjl.symm)).elim · subst l simp [hij, Ne.symm hij] <;> try ring <;> simp_all · by_cases hjl : j = l · subst l simp [hij, Ne.symm hij] <;> try ring <;> simp_all · simp [hil, Ne.symm hil, hjl, Ne.symm hjl] <;> try ring <;> simp_all _ = _ := by rw [Finset.sum_add_distrib] simp ring -
deformedShift_apply_secondtheorem — When the selected coordinates are distinct, the second transformed shift is its stated nonnegative weighted sum.hypothesesconclusiondeformedShift B i j u v t s j= (secondNormalizationDenom B i j u t)⁻¹ ^ 2 * (t ^ 2 * u ^ 2 * s i + s j)Proof (Lean source)
theorem deformedShift_apply_second {d : ℕ} (B : SqMatrix d) {i j : Fin d} (hij : i ≠ j) (u v t : ℝ) (s : Fin d → ℝ) : deformedShift B i j u v t s j = (secondNormalizationDenom B i j u t)⁻¹ ^ 2 * (t ^ 2 * u ^ 2 * s i + s j) := by classical rw [deformedShift_sum_squares] simp only [normalizedPairDeformation_apply] simp only [if_neg (Ne.symm hij), if_pos, hij, false_and, if_false, true_and] calc _ = ∑ l, ((if i = l then (secondNormalizationDenom B i j u t)⁻¹ ^ 2 * (t ^ 2 * u ^ 2) * s l else 0) + (if j = l then (secondNormalizationDenom B i j u t)⁻¹ ^ 2 * s l else 0)) := by apply Finset.sum_congr rfl intro l hl by_cases hil : i = l · by_cases hjl : j = l · exact (hij (hil.trans hjl.symm)).elim · subst l simp [hij, Ne.symm hij] <;> try ring <;> simp_all · by_cases hjl : j = l · subst l simp [hij, Ne.symm hij] <;> try ring <;> simp_all · simp [hil, Ne.symm hil, hjl, Ne.symm hjl] <;> try ring <;> simp_all _ = _ := by rw [Finset.sum_add_distrib] simp ring -
deformedShift_apply_of_netheorem — When the coordinate is neither selected coordinate, its transformed shift is unchanged.hypothesesconclusiondeformedShift B i j u v t s k = s kProof (Lean source)
theorem deformedShift_apply_of_ne {d : ℕ} (B : SqMatrix d) {i j k : Fin d} (hki : k ≠ i) (hkj : k ≠ j) (u v t : ℝ) (s : Fin d → ℝ) : deformedShift B i j u v t s k = s k := by classical rw [deformedShift_sum_squares] simp [normalizedPairDeformation_apply, hki, hkj, Ne.symm hki, Ne.symm hkj] -
deformedShift_nonnegativetheorem — When the selected coordinates are distinct and the original shift is coordinatewise nonnegative, the transformed shift is coordinatewise nonnegative.hypothesesconclusion0 ≤ deformedShift B i j u v t s kProof (Lean source)
theorem deformedShift_nonnegative {d : ℕ} (B : SqMatrix d) {i j : Fin d} (hij : i ≠ j) (u v t : ℝ) (s : Fin d → ℝ) (hs : ∀ k, 0 ≤ s k) : ∀ k, 0 ≤ deformedShift B i j u v t s k := by intro k by_cases hki : k = i · subst k rw [deformedShift_apply_first B hij] exact mul_nonneg (sq_nonneg _) (add_nonneg (hs i) (mul_nonneg (mul_nonneg (sq_nonneg t) (sq_nonneg v)) (hs j))) · by_cases hkj : k = j · subst k rw [deformedShift_apply_second B hij] exact mul_nonneg (sq_nonneg _) (add_nonneg (mul_nonneg (mul_nonneg (sq_nonneg t) (sq_nonneg u)) (hs i)) (hs j)) · rw [deformedShift_apply_of_ne B hki hkj] exact hs k -
pairShear_diagonal_congruence_decompositiontheorem — When the selected coordinates are distinct, the transformed diagonal shift matrix splits into the common symmetric off-diagonal term and its new diagonal shift.hypothesesd :ℕE :Type*B :SqMatrix di j :Fin dhij :i ≠ js :E → Fin d → ℝcert :AffineLineCertificate s i jt :ℝe :EconclusionT :normalizedPairDeformation B i j cert.u cert.v tT * diagonal (s e) * T.transpose= pairSymmetricOffDiagonal i j (commonShiftCrossTerm B i j cert.u cert.v cert.c t)+ diagonal (deformedShift B i j cert.u cert.v t (s e))Proof (Lean source)
theorem pairShear_diagonal_congruence_decomposition {d : ℕ} {E : Type*} (B : SqMatrix d) {i j : Fin d} (hij : i ≠ j) (s : E → Fin d → ℝ) (cert : AffineLineCertificate s i j) (t : ℝ) (e : E) : let T := normalizedPairDeformation B i j cert.u cert.v t T * diagonal (s e) * T.transpose = pairSymmetricOffDiagonal i j (commonShiftCrossTerm B i j cert.u cert.v cert.c t) + diagonal (deformedShift B i j cert.u cert.v t (s e)) := by classical dsimp ext a b by_cases hab : a = b · subst b have hia : ¬(i = a ∧ j = a) := by rintro ⟨rfl, h⟩ exact hij h.symm have hja : ¬(j = a ∧ i = a) := by rintro ⟨rfl, h⟩ exact hij h simp [pairSymmetricOffDiagonal, Matrix.single_apply, hia, hja, deformedShift] · by_cases hai : a = i · subst a by_cases hbj : b = j · subst b simpa [pairSymmetricOffDiagonal, hij, Ne.symm hij] using diagonal_congruence_apply_first_second B hij s cert t e · have hbi : b ≠ i := by intro h; exact hab h.symm have hz := diagonal_congruence_apply_unselected B hbi hbj (Ne.symm hab) cert.u cert.v t (s e) rw [diagonal_congruence_symm_apply] simpa [pairSymmetricOffDiagonal, Matrix.single_apply, hij, Ne.symm hij, hbi, Ne.symm hbi, hbj, Ne.symm hbj, hab, Ne.symm hab] using hz · by_cases haj : a = j · subst a by_cases hbi : b = i · subst b simpa [pairSymmetricOffDiagonal, hij, Ne.symm hij] using diagonal_congruence_apply_second_first B hij s cert t e · have hbj : b ≠ j := by intro h; exact hab h.symm have hz := diagonal_congruence_apply_unselected B hbi hbj (Ne.symm hab) cert.u cert.v t (s e) rw [diagonal_congruence_symm_apply] simpa [pairSymmetricOffDiagonal, Matrix.single_apply, hij, Ne.symm hij, hbi, Ne.symm hbi, hbj, Ne.symm hbj, hab, Ne.symm hab] using hz · by_cases hbi : b = i · subst b have hz := diagonal_congruence_apply_unselected B hai haj hab cert.u cert.v t (s e) simpa [pairSymmetricOffDiagonal, Matrix.single_apply, hij, Ne.symm hij, hai, Ne.symm hai, haj, Ne.symm haj, hab, Ne.symm hab] using hz · by_cases hbj : b = j · subst b have hz := diagonal_congruence_apply_unselected B hai haj hab cert.u cert.v t (s e) simpa [pairSymmetricOffDiagonal, Matrix.single_apply, hij, Ne.symm hij, hai, Ne.symm hai, haj, Ne.symm haj, hab, Ne.symm hab] using hz · have hz := diagonal_congruence_apply_unselected B hai haj hab cert.u cert.v t (s e) simpa [pairSymmetricOffDiagonal, Matrix.single_apply, hij, Ne.symm hij, hai, Ne.symm hai, haj, Ne.symm haj, hbi, Ne.symm hbi, hbj, Ne.symm hbj, hab, Ne.symm hab] using hz -
total_congruence_decompositiontheorem — When the selected coordinates are distinct, the latent congruence is exactly the deformed invariant plus the transformed diagonal shift.hypothesesd :ℕE :Type*B Ω :SqMatrix di j :Fin dhij :i ≠ js :E → Fin d → ℝcert :AffineLineCertificate s i jt :ℝe :EconclusionT :normalizedPairDeformation B i j cert.u cert.v tT * (Ω + diagonal (s e)) * T.transpose= deformedInvariant B Ω i j cert.u cert.v cert.c t+ diagonal (deformedShift B i j cert.u cert.v t (s e))Proof (Lean source)
theorem total_congruence_decomposition {d : ℕ} {E : Type*} (B Ω : SqMatrix d) {i j : Fin d} (hij : i ≠ j) (s : E → Fin d → ℝ) (cert : AffineLineCertificate s i j) (t : ℝ) (e : E) : let T := normalizedPairDeformation B i j cert.u cert.v t T * (Ω + diagonal (s e)) * T.transpose = deformedInvariant B Ω i j cert.u cert.v cert.c t + diagonal (deformedShift B i j cert.u cert.v t (s e)) := by dsimp rw [mul_add, add_mul] rw [pairShear_diagonal_congruence_decomposition B hij s cert t e] simp only [deformedInvariant] noncomm_ring -
representedCovariance_posDeftheorem — An invertible representation with positive invariant and nonnegative shifts produces a positive-definite covariance, for diagonalizer B, invariant Ω, and shift s in dimension d, under invertibility, positive definiteness, and coordinatewise nonnegativity.hypothesesconclusion(representedCovariance B Ω s).PosDefProof (Lean source)
theorem representedCovariance_posDef {d : ℕ} (B Ω : SqMatrix d) (s : Fin d → ℝ) (hB : IsUnit B.det) (hΩ : Ω.PosDef) (hs : ∀ k, 0 ≤ s k) : (representedCovariance B Ω s).PosDef := by have hsum : (Ω + diagonal s).PosDef := hΩ.add_posSemidef (Matrix.PosSemidef.diagonal hs) have hBinv : IsUnit B⁻¹ := (Matrix.isUnit_iff_isUnit_det B⁻¹).mpr (Matrix.isUnit_nonsing_inv_det B hB) have hinj : Injective B⁻¹.vecMul := Matrix.vecMul_injective_iff_isUnit.mpr hBinv simpa [representedCovariance] using hsum.mul_mul_conjTranspose_same hinj -
deformedInvariant_isSymmtheorem — When the original invariant is symmetric, the deformed invariant is symmetric.hypothesesconclusion(deformedInvariant B Ω i j u v c t).IsSymmProof (Lean source)
theorem deformedInvariant_isSymm {d : ℕ} (B Ω : SqMatrix d) {i j : Fin d} (hΩ : Ω.IsSymm) (u v c t : ℝ) : (deformedInvariant B Ω i j u v c t).IsSymm := by unfold deformedInvariant apply Matrix.IsSymm.add · simp only [IsSymm, Matrix.transpose_mul, Matrix.transpose_transpose] rw [hΩ, Matrix.mul_assoc] · simp [pairSymmetricOffDiagonal, IsSymm, add_comm]
LocalBranch 1 core · 5 supporting This module converts an ordinary entrywise-L² neighborhood of the reference into control of the transition error. ★ inIdentityBranch_of_small_residual
Local branch selection for pairwise-affine congruence stability
This module converts an ordinary entrywise-L² neighborhood of the reference into control of the transition error. It then combines that control with an explicit small-residual threshold and the pairwise quadratic estimate to select the identity branch. Thus the stability API does not ask callers to assume the desired transition-error bound directly.
theorem inIdentityBranch_of_small_residual reviewed
⚑ flagged
Causalean.Discovery.LinearDisentanglement.SimultaneousCongruence
Small-residual local identity-branch selection. For positive dimension, shift scale, affine margin, matrix scale, and inverse envelope, bounded pairwise-separated shifts, an exact invertible unit-diagonal reference, a unit-diagonal candidate, a reference operator norm at most the matrix scale, an inverse bound, nonnegative approximate residual, the explicit residual smallness condition, and membership in the explicit ordinary reference neighborhood, the transition lies on the identity branch needed by the linear stability estimate.
Formal statement
hypotheses
p :
ℕ
E :
A :
E → SqMatrix p
s :
E → Fin p → ℝ
B₀ B :
SqMatrix p
M δ L J ε :
ℝ
hp :
0 < p
hM :
0 < M
hδ :
0 < δ
hL :
1 ≤ L
hJ :
0 < J
hscale :
ShiftScaleBound s M
hsep :
hunit :
IsUnit B₀.det
hexact :
ExactCongruence A s B₀
hdiag₀ :
UnitDiagonal B₀
hdiag :
hB₀ :
‖B₀‖ ≤ L
hinv :
‖B₀⁻¹‖ ≤ J
hε :
0 ≤ ε
hsmall :
ε ≤ pairwiseResidualRadius p M δ L
happrox :
hlocal :
InReferenceNeighborhood (pairwiseLocalRadius p M δ L J) B₀ B
conclusion
InIdentityBranch M δ L B₀ B
Proof (Lean source)
-- Proof route: the neighborhood and inverse envelope give `u ≤ min 1 (3/(8 max(1,K)M))`
-- for `u = entryL2 R`. Pairwise control gives `u ≤ 2 K M u² + 2 K ε`; the coarse
-- local bound absorbs three quarters of `u`, and the residual radius improves this to
-- `2 K M u ≤ 1/2`. This derives, rather than assumes, `InIdentityBranch`.
theorem inIdentityBranch_of_small_residual {p : ℕ} {E : Type*}
[Fintype E] [Nonempty E]
(A : E → SqMatrix p) (s : E → Fin p → ℝ) (B₀ B : SqMatrix p)
{M δ L J ε : ℝ}
(hp : 0 < p) (hM : 0 < M) (hδ : 0 < δ) (hL : 1 ≤ L) (hJ : 0 < J)
(hscale : ShiftScaleBound s M) (hsep : PairwiseAffineSeparated s δ)
(hunit : IsUnit B₀.det) (hexact : ExactCongruence A s B₀)
(hdiag₀ : UnitDiagonal B₀) (hdiag : UnitDiagonal B)
(hB₀ : ‖B₀‖ ≤ L) (hinv : ‖B₀⁻¹‖ ≤ J)
(hε : 0 ≤ ε) (hsmall : ε ≤ pairwiseResidualRadius p M δ L)
(happrox : OffDiagonalApproximateCongruence A B ε)
(hlocal : InReferenceNeighborhood (pairwiseLocalRadius p M δ L J) B₀ B) :
InIdentityBranch M δ L B₀ B := by
let R := transitionError B₀ B
let u := entryL2 R
let K := pairwiseAggregateFactor p M δ L
have hpR : (0 : ℝ) < p := by exact_mod_cast hp
have hL0 : 0 ≤ L := le_trans (by norm_num) hL
have hK0 : 0 ≤ K := by
dsimp [K, pairwiseAggregateFactor, pairwiseSolveFactor]
positivity
have hmax : 0 < max 1 K := lt_of_lt_of_le (by norm_num) (le_max_left _ _)
have hKmax : K ≤ max 1 K := le_max_right _ _
have hu0 : 0 ≤ u := by
exact entryL2_nonneg R
have huLocal : u ≤ min 1 (3 / (8 * max 1 K * M)) := by
have h := transitionError_entryL2_le_of_neighborhood B₀ B hp
hunit hinv hlocal
change u ≤ (p : ℝ) * J * pairwiseLocalRadius p M δ L J at h
calc
u ≤ (p : ℝ) * J * pairwiseLocalRadius p M δ L J := h
_ = min 1 (3 / (8 * max 1 K * M)) := by
dsimp [pairwiseLocalRadius, K]
field_simp
have hu1 : u ≤ 1 := huLocal.trans (min_le_left _ _)
have huCoarse : u ≤ 3 / (8 * max 1 K * M) :=
huLocal.trans (min_le_right _ _)
have hc0 : 0 ≤ pairwiseSolveFactor M δ *
(2 * M * u ^ 2 + 2 * ε) := by
unfold pairwiseSolveFactor
positivity
have hoff : ∀ i j, i ≠ j →
|R i j| ≤ pairwiseSolveFactor M δ * (2 * M * u ^ 2 + 2 * ε) := by
simpa [R, u] using pairwise_offDiagonal_control A s B₀ B hM.le hδ hε
hscale hsep hunit hexact happrox
have huAgg := entryL2_transitionError_le B₀ B hp hL0 hc0 hunit hdiag₀ hdiag
hB₀ hoff
have huK : u ≤ K * (2 * M * u ^ 2 + 2 * ε) := by
change u ≤ pairwiseSolveFactor M δ * (2 * M * u ^ 2 + 2 * ε) *
sqrt ((p : ℝ) * (p - 1 : ℕ) * (1 + L ^ 2)) at huAgg
calc
u ≤ pairwiseSolveFactor M δ * (2 * M * u ^ 2 + 2 * ε) *
sqrt ((p : ℝ) * (p - 1 : ℕ) * (1 + L ^ 2)) := huAgg
_ = K * (2 * M * u ^ 2 + 2 * ε) := by
dsimp [K, pairwiseAggregateFactor]
ring
have hcoefficient : 2 * K * M * u ≤ 3 / 4 := by
calc
2 * K * M * u ≤ 2 * (max 1 K) * M * u := by gcongr
_ ≤ 2 * (max 1 K) * M * (3 / (8 * max 1 K * M)) := by gcongr
_ = 3 / 4 := by field_simp; ring
have huLinear : u ≤ 8 * K * ε := by
have hquad : 2 * K * M * u ^ 2 ≤ (3 / 4) * u := by
nlinarith [mul_nonneg hu0 (sub_nonneg.mpr hcoefficient)]
nlinarith
have hsmall' : ε ≤ 1 / (32 * (max 1 K) ^ 2 * M) := by
simpa [pairwiseResidualRadius, K] using hsmall
have hbranch : 2 * K * M * u ≤ 1 / 2 := by
calc
2 * K * M * u ≤ 2 * K * M * (8 * K * ε) := by gcongr
_ = 16 * K ^ 2 * M * ε := by ring
_ ≤ 16 * (max 1 K) ^ 2 * M * ε := by
gcongr
_ ≤ 16 * (max 1 K) ^ 2 * M *
(1 / (32 * (max 1 K) ^ 2 * M)) := by gcongr
_ = 1 / 2 := by field_simp; ring
exact ⟨by simpa [u, R] using hu1, by simpa [u, R, K] using hbranch⟩
5 supporting declarations (lemmas, instances)
-
entryL2_mul_letheorem — Entrywise Euclidean size is submultiplicative, so errors do not amplify beyond the product of the sizes of matrices X and Y in dimension p.Proof (Lean source)
theorem entryL2_mul_le {p : ℕ} (X Y : SqMatrix p) : entryL2 (X * Y) ≤ entryL2 X * entryL2 Y := by exact Matrix.frobenius_norm_mul X Y -
entryL2_le_dimension_mul_opNormtheorem — Entrywise Euclidean size is at most dimension times operator norm for matrix X in dimension p, provided the dimension is positive.Proof (Lean source)
theorem entryL2_le_dimension_mul_opNorm {p : ℕ} (X : SqMatrix p) (hp : 0 < p) : entryL2 X ≤ (p : ℝ) * ‖X‖ := by rw [entryL2_eq_sqrt, Real.sqrt_le_iff] constructor · positivity · calc ∑ i, ∑ j, |X i j| ^ 2 ≤ ∑ _i : Fin p, ∑ _j : Fin p, ‖X‖ ^ 2 := by gcongr with i j exact abs_entry_le_opNorm X i j _ = ((p : ℝ) * ‖X‖) ^ 2 := by simp [Finset.sum_const, nsmul_eq_mul] ring -
transitionError_eq_sub_mul_invtheorem — Transition error is the candidate-reference discrepancy expressed in reference coordinates, for reference and candidate matrices in dimension p when the reference is invertible.hypothesesconclusiontransitionError B₀ B = (B - B₀) * B₀⁻¹Proof (Lean source)
theorem transitionError_eq_sub_mul_inv {p : ℕ} (B₀ B : SqMatrix p) (hunit : IsUnit B₀.det) : transitionError B₀ B = (B - B₀) * B₀⁻¹ := by unfold transitionError transition rw [Matrix.sub_mul, Matrix.mul_nonsing_inv B₀ hunit] -
transitionError_entryL2_le_of_neighborhoodtheorem — A local candidate neighborhood yields a quantitative transition-error bound for reference and candidate matrices in dimension p, with inverse envelope J and radius ρ, positive dimension, invertible reference, bounded reference inverse, and local proximity.hypothesesp :ℕB₀ B :SqMatrix pJ ρ :ℝhp :0 < phunit :IsUnit B₀.dethinv :‖B₀⁻¹‖ ≤ Jhlocal :InReferenceNeighborhood ρ B₀ BconclusionentryL2 (transitionError B₀ B) ≤ (p : ℝ) * J * ρProof (Lean source)
theorem transitionError_entryL2_le_of_neighborhood {p : ℕ} (B₀ B : SqMatrix p) {J ρ : ℝ} (hp : 0 < p) (hunit : IsUnit B₀.det) (hinv : ‖B₀⁻¹‖ ≤ J) (hlocal : InReferenceNeighborhood ρ B₀ B) : entryL2 (transitionError B₀ B) ≤ (p : ℝ) * J * ρ := by rw [transitionError_eq_sub_mul_inv B₀ B hunit] calc entryL2 ((B - B₀) * B₀⁻¹) ≤ entryL2 (B - B₀) * entryL2 B₀⁻¹ := entryL2_mul_le _ _ _ ≤ ρ * ((p : ℝ) * J) := by have hρ : 0 ≤ ρ := (entryL2_nonneg _).trans hlocal apply mul_le_mul hlocal · exact (entryL2_le_dimension_mul_opNorm B₀⁻¹ hp).trans (mul_le_mul_of_nonneg_left hinv (by positivity)) · exact entryL2_nonneg _ · exact hρ _ = (p : ℝ) * J * ρ := by ring -
invOpNorm_le_conditionEnvelopetheorem — A unit-diagonal determinant-condition certificate bounds the inverse operator norm for matrix B in dimension p under condition envelope κ, assuming positive dimension, unit diagonal, and the certificate.hypothesesconclusion‖B⁻¹‖ ≤ κProof (Lean source)
theorem invOpNorm_le_conditionEnvelope {p : ℕ} {κ : ℝ} (B : SqMatrix p) (hp : 0 < p) (hdiag : UnitDiagonal B) (henv : DetConditionEnvelope κ B) : ‖B⁻¹‖ ≤ κ := by letI : Nonempty (Fin p) := Fin.pos_iff_nonempty.mp hp let i : Fin p := choice (inferInstance : Nonempty (Fin p)) have hB : 1 ≤ ‖B‖ := by simpa [hdiag i] using abs_entry_le_opNorm B i i calc ‖B⁻¹‖ ≤ ‖B‖ * ‖B⁻¹‖ := by nlinarith [norm_nonneg B⁻¹] _ = operatorConditionNumber B := rfl _ ≤ κ := henv.2.2
Main 1 core · 1 supporting This module gives a paper-independent non-identifiability witness for a family (over any index set) of positive-definite covariance matrices. ★ exists_collinear_simultaneous_congruence_ambiguity
Constructive ambiguity from an affine-collinear shift pair
This module gives a paper-independent non-identifiability witness for a family (over any index set) of positive-definite covariance matrices. If two selected coordinates of all diagonal shifts lie on one affine line, an arbitrarily small nonzero normalized two-row deformation produces a distinct invertible diagonalizer and a second exact positive-definite/nonnegative representation of the same family.
theorem exists_collinear_simultaneous_congruence_ambiguity reviewed
⚑ flagged
Causalean.Discovery.LinearDisentanglement.SimultaneousCongruence
Affine collinearity of two shift coordinates creates an arbitrarily small continuum of observationally equivalent, admissible representations. For dimension d, environment type E, reference diagonalizer B₀, invariant Ω₀, shifts s, and selected coordinates i,j, this uses distinct coordinates, unit diagonal and invertibility, pair-cycle admissibility, positive-definite invariant, nonnegative shifts, an affine-line certificate, and positive radius r.
Formal statement
hypotheses
d :
ℕ
E :
Type*
B₀ Ω₀ :
SqMatrix d
s :
E → Fin d → ℝ
i j :
Fin d
hij :
i ≠ j
hdiag :
UnitDiagonal B₀
hunit :
IsUnit B₀.det
hcycle :
PairCycleAdmissible B₀ i j
hΩ :
Ω₀.PosDef
hs :
∀ e k, 0 ≤ s e k
cert :
AffineLineCertificate s i j
r :
ℝ
hr :
0 < r
conclusion
0 < |t|
|t| < r
B₁ = deformedDiagonalizer B₀ i j cert.u cert.v t
Ω₁ = deformedInvariant B₀ Ω₀ i j cert.u cert.v cert.c t
s₁ = (fun e ↦ deformedShift B₀ i j cert.u cert.v t (s e))
UnitDiagonal B₁
IsUnit B₁.det
PairCycleAdmissible B₁ i j
B₁ ≠ B₀
Ω₁.IsSymm
Ω₁.PosDef
conclusion 1
e k :
0 ≤ s₁ e k
Proof (Lean source)
theorem exists_collinear_simultaneous_congruence_ambiguity
{d : ℕ} {E : Type*}
(B₀ Ω₀ : SqMatrix d) (s : E → Fin d → ℝ) {i j : Fin d}
(hij : i ≠ j) (hdiag : UnitDiagonal B₀) (hunit : IsUnit B₀.det)
(hcycle : PairCycleAdmissible B₀ i j) (hΩ : Ω₀.PosDef)
(hs : ∀ e k, 0 ≤ s e k) (cert : AffineLineCertificate s i j)
{r : ℝ} (hr : 0 < r) :
∃ (t : ℝ) (B₁ Ω₁ : SqMatrix d) (s₁ : E → Fin d → ℝ),
0 < |t| ∧ |t| < r ∧
B₁ = deformedDiagonalizer B₀ i j cert.u cert.v t ∧
Ω₁ = deformedInvariant B₀ Ω₀ i j cert.u cert.v cert.c t ∧
s₁ = (fun e ↦ deformedShift B₀ i j cert.u cert.v t (s e)) ∧
UnitDiagonal B₁ ∧ IsUnit B₁.det ∧ PairCycleAdmissible B₁ i j ∧
B₁ ≠ B₀ ∧ Ω₁.IsSymm ∧ Ω₁.PosDef ∧
(∀ e k, 0 ≤ s₁ e k) ∧
(∀ e, (representedCovariance B₀ Ω₀ (s e)).PosDef) ∧
∀ e,
representedCovariance B₁ Ω₁ (s₁ e) =
representedCovariance B₀ Ω₀ (s e) := by
rcases exists_small_admissible_parameter B₀ Ω₀ hij hdiag hunit hcycle hΩ
s cert.u cert.v cert.c cert.normal_ne hs hr with
⟨t, ht0, htr, _hfirst, _hsecond, _hdet, hTunit, hB₁unit,
hB₁diag, hB₁cycle, hB₁ne, hΩ₁pos, hs₁⟩
refine ⟨t,
deformedDiagonalizer B₀ i j cert.u cert.v t,
deformedInvariant B₀ Ω₀ i j cert.u cert.v cert.c t,
(fun e ↦ deformedShift B₀ i j cert.u cert.v t (s e)),
ht0, htr, rfl, rfl, rfl, hB₁diag, hB₁unit, hB₁cycle, hB₁ne, ?_,
hΩ₁pos, hs₁, ?_, ?_⟩
· have hΩsymm : Ω₀.IsSymm := by
rw [← Matrix.isHermitian_iff_isSymm]
exact hΩ.isHermitian
exact deformedInvariant_isSymm B₀ Ω₀ hΩsymm
cert.u cert.v cert.c t
· intro e
exact representedCovariance_posDef B₀ Ω₀ (s e) hunit hΩ (hs e)
· intro e
exact representedCovariance_deformation_eq B₀ Ω₀ hij s cert t e hTunit
1 supporting declaration (lemmas, instances)
-
exists_interior_collinear_ambiguity_exampletheorem — Every nonnegative affine-collinear shift family admits a positive-definite covariance family with two distinct normalized diagonalizers, providing a concrete interior nonidentification example. It applies to dimension d, environment type E, shift family s, and coordinates i,j, assuming the coordinates are distinct, the shifts are nonnegative, and their pair lies on a certified affine line.hypothesesd :ℕE :Type*s :E → Fin d → ℝi j :Fin dhij :i ≠ jhs :∀ e k, 0 ≤ s e kcert :AffineLineCertificate s i jconclusionB₀ = 1Ω₀ = 1UnitDiagonal B₀IsUnit B₀.detPairCycleAdmissible B₀ i jUnitDiagonal B₁IsUnit B₁.detPairCycleAdmissible B₁ i jB₁ ≠ B₀Ω₀.PosDefΩ₁.IsSymmΩ₁.PosDefconclusion 1e k :0 ≤ s₁ e kconclusion 3RepresentsCovarianceFamily Sigma B₀ Ω₀ sconclusion 4RepresentsCovarianceFamily Sigma B₁ Ω₁ s₁Proof (Lean source)
theorem exists_interior_collinear_ambiguity_example {d : ℕ} {E : Type*} (s : E → Fin d → ℝ) {i j : Fin d} (hij : i ≠ j) (hs : ∀ e k, 0 ≤ s e k) (cert : AffineLineCertificate s i j) : ∃ (Sigma : E → SqMatrix d) (B₀ B₁ Ω₀ Ω₁ : SqMatrix d) (s₁ : E → Fin d → ℝ), B₀ = 1 ∧ Ω₀ = 1 ∧ UnitDiagonal B₀ ∧ IsUnit B₀.det ∧ PairCycleAdmissible B₀ i j ∧ UnitDiagonal B₁ ∧ IsUnit B₁.det ∧ PairCycleAdmissible B₁ i j ∧ B₁ ≠ B₀ ∧ Ω₀.PosDef ∧ Ω₁.IsSymm ∧ Ω₁.PosDef ∧ (∀ e k, 0 ≤ s₁ e k) ∧ (∀ e, (Sigma e).PosDef) ∧ RepresentsCovarianceFamily Sigma B₀ Ω₀ s ∧ RepresentsCovarianceFamily Sigma B₁ Ω₁ s₁ := by have hdiag₀ : UnitDiagonal (1 : SqMatrix d) := by intro k simp have hunit₀ : IsUnit (1 : SqMatrix d).det := by simp have hcycle₀ : PairCycleAdmissible (1 : SqMatrix d) i j := by simp [PairCycleAdmissible, hij] have hΩ₀ : (1 : SqMatrix d).PosDef := Matrix.PosDef.one rcases exists_collinear_simultaneous_congruence_ambiguity (1 : SqMatrix d) (1 : SqMatrix d) s hij hdiag₀ hunit₀ hcycle₀ hΩ₀ hs cert (r := 1) (by norm_num) with ⟨t, B₁, Ω₁, s₁, _ht0, _htr, _hB₁eq, _hΩ₁eq, _hs₁eq, hB₁diag, hB₁unit, hB₁cycle, hB₁ne, hΩ₁symm, hΩ₁pos, hs₁, hSigmaPos, hrepEq⟩ refine ⟨(fun e ↦ representedCovariance (1 : SqMatrix d) (1 : SqMatrix d) (s e)), 1, B₁, 1, Ω₁, s₁, rfl, rfl, hdiag₀, hunit₀, hcycle₀, hB₁diag, hB₁unit, hB₁cycle, hB₁ne, hΩ₀, hΩ₁symm, hΩ₁pos, hs₁, hSigmaPos, ?_, ?_⟩ · intro e rfl · intro e exact (hrepEq e).symm
PairwiseControl 1 core · 5 supporting This module expands a congruence around the identity transition, bounds its quadratic coordinate-product remainder, solves the two-coordinate affine system furnished by one pair's selected environment triple, and control ★ pairwise_offDiagonal_control
Pairwise affine coordinate control
This module expands a congruence around the identity transition, bounds its quadratic coordinate-product remainder, solves the two-coordinate affine system furnished by one pair's selected environment triple, and controls diagonal transition entries using unit-diagonal normalization.
theorem pairwise_offDiagonal_control reviewed
⚑ flagged
Causalean.Discovery.LinearDisentanglement.SimultaneousCongruence
Pairwise affine separation gives one common bound for every off-diagonal transition error, for matrix family, shifts, reference, and candidate over environments E in dimension p, with scale, margin, and residual parameters, nonnegative scale and residual with positive margin, bounded separated shifts, an invertible exact reference, and an approximately diagonal candidate.
Formal statement
hypotheses
p :
ℕ
E :
A :
E → SqMatrix p
s :
E → Fin p → ℝ
B₀ B :
SqMatrix p
M δ ε :
ℝ
hM :
0 ≤ M
hδ :
0 < δ
hε :
0 ≤ ε
hscale :
ShiftScaleBound s M
hsep :
hunit :
IsUnit B₀.det
hexact :
ExactCongruence A s B₀
happrox :
i j :
i ≠ j
conclusion
|transitionError B₀ B i j|
Proof (Lean source)
theorem pairwise_offDiagonal_control {p : ℕ} {E : Type*}
[Fintype E] [Nonempty E]
(A : E → SqMatrix p) (s : E → Fin p → ℝ) (B₀ B : SqMatrix p)
{M δ ε : ℝ} (hM : 0 ≤ M) (hδ : 0 < δ) (hε : 0 ≤ ε)
(hscale : ShiftScaleBound s M) (hsep : PairwiseAffineSeparated s δ)
(hunit : IsUnit B₀.det) (hexact : ExactCongruence A s B₀)
(happrox : OffDiagonalApproximateCongruence A B ε) :
∀ i j, i ≠ j →
|transitionError B₀ B i j| ≤
pairwiseSolveFactor M δ *
(2 * M * entryL2 (transitionError B₀ B) ^ 2 + 2 * ε) := by
intro i j hij
obtain ⟨e₀, e₁, e₂, hdet⟩ := hsep i j hij
exact (selectedTriple_offDiagonal_control A s B₀ B i j hij e₀ e₁ e₂
hM hδ hε hscale hdet hunit hexact happrox).1
5 supporting declarations (lemmas, instances)
-
coordinateProductRemainder_letheorem — The nonlinear coordinate-product remainder is quadratic in transition error, so it is lower order near the reference. This holds for error matrix R, rows i,j, environments e₁,e₀, and shift family s over environment type E in dimension p, under scale M, nonnegativity, and the shift bound.hypothesesp :ℕE :Type*Fintype Es :E → Fin p → ℝR :SqMatrix pM :ℝhM :0 ≤ Mhscale :ShiftScaleBound s Me₁ e₀ :Ei j :Fin pconclusion|∑ k, R i k * R j k * (s e₁ k - s e₀ k)| ≤ 2 * M * entryL2 R ^ 2Proof (Lean source)
-- Proof route: `|s₁ k-s₀ k| ≤ 2M`, then Cauchy--Schwarz on the two rows and the -- fact that each row's squared sum is bounded by the full entrywise squared sum. theorem coordinateProductRemainder_le {p : ℕ} {E : Type*} [Fintype E] (s : E → Fin p → ℝ) (R : SqMatrix p) {M : ℝ} (hM : 0 ≤ M) (hscale : ShiftScaleBound s M) (e₁ e₀ : E) (i j : Fin p) : |∑ k, R i k * R j k * (s e₁ k - s e₀ k)| ≤ 2 * M * entryL2 R ^ 2 := by classical have hshift (k : Fin p) : |s e₁ k - s e₀ k| ≤ 2 * M := by calc |s e₁ k - s e₀ k| ≤ |s e₁ k| + |s e₀ k| := abs_sub _ _ _ ≤ M + M := add_le_add (hscale _ _) (hscale _ _) _ = 2 * M := by ring have hterm (k : Fin p) : |R i k * R j k * (s e₁ k - s e₀ k)| ≤ M * (|R i k| ^ 2 + |R j k| ^ 2) := by have huv : 2 * (|R i k| * |R j k|) ≤ |R i k| ^ 2 + |R j k| ^ 2 := by nlinarith [sq_nonneg (|R i k| - |R j k|)] calc |R i k * R j k * (s e₁ k - s e₀ k)| = (|R i k| * |R j k|) * |s e₁ k - s e₀ k| := by simp only [abs_mul] _ ≤ (|R i k| * |R j k|) * (2 * M) := by gcongr exact hshift k _ ≤ M * (|R i k| ^ 2 + |R j k| ^ 2) := by nlinarith [mul_nonneg (abs_nonneg (R i k)) (abs_nonneg (R j k))] have hrow (a : Fin p) : (∑ k, |R a k| ^ 2) ≤ ∑ u, ∑ k, |R u k| ^ 2 := by exact Finset.single_le_sum (fun u _ => Finset.sum_nonneg fun k _ => sq_nonneg |R u k|) (Finset.mem_univ a) have hentry : entryL2 R ^ 2 = ∑ u, ∑ k, |R u k| ^ 2 := by rw [entryL2_eq_sqrt, Real.sq_sqrt] positivity calc |∑ k, R i k * R j k * (s e₁ k - s e₀ k)| ≤ ∑ k, |R i k * R j k * (s e₁ k - s e₀ k)| := Finset.abs_sum_le_sum_abs _ _ _ ≤ ∑ k, M * (|R i k| ^ 2 + |R j k| ^ 2) := by gcongr with k exact hterm k _ = M * ((∑ k, |R i k| ^ 2) + ∑ k, |R j k| ^ 2) := by simp_rw [mul_add] rw [Finset.sum_add_distrib, ← Finset.mul_sum, ← Finset.mul_sum] _ ≤ 2 * M * (∑ u, ∑ k, |R u k| ^ 2) := by nlinarith [hrow i, hrow j] _ = 2 * M * entryL2 R ^ 2 := by rw [hentry] -
pair_cramer_controltheorem — If the scale is nonnegative, the determinant margin is positive, and the residual bound is nonnegative, all four coefficients have scale at most 2M, the two-by-two coefficient determinant is separated, the two displayed equations hold, and both equation residuals are at most η, then both unknowns obey the conservative explicit Cramer bound.hypothesesa b c d x y r₁ r₂ M δ η :ℝhM :0 ≤ Mhδ :0 < δhη :0 ≤ ηhcoeff :|a| ≤ 2 * M ∧ |b| ≤ 2 * M ∧ |c| ≤ 2 * M ∧ |d| ≤ 2 * Mhdet :δ ≤ |a * d - c * b|heq₁ :a * x + b * y = r₁heq₂ :c * x + d * y = r₂hr₁ :|r₁| ≤ ηhr₂ :|r₂| ≤ ηconclusionconclusion 1|x| ≤ pairwiseSolveFactor M δ * ηconclusion 2|y| ≤ pairwiseSolveFactor M δ * ηProof (Lean source)
theorem pair_cramer_control {a b c d x y r₁ r₂ M δ η : ℝ} (hM : 0 ≤ M) (hδ : 0 < δ) (hη : 0 ≤ η) (hcoeff : |a| ≤ 2 * M ∧ |b| ≤ 2 * M ∧ |c| ≤ 2 * M ∧ |d| ≤ 2 * M) (hdet : δ ≤ |a * d - c * b|) (heq₁ : a * x + b * y = r₁) (heq₂ : c * x + d * y = r₂) (hr₁ : |r₁| ≤ η) (hr₂ : |r₂| ≤ η) : |x| ≤ pairwiseSolveFactor M δ * η ∧ |y| ≤ pairwiseSolveFactor M δ * η := by have hxid : (a * d - c * b) * x = d * r₁ - b * r₂ := by rw [← heq₁, ← heq₂] ring_nf have hyid : (a * d - c * b) * y = a * r₂ - c * r₁ := by rw [← heq₁, ← heq₂] ring have hxnum : |d * r₁ - b * r₂| ≤ 4 * M * η := by calc |d * r₁ - b * r₂| ≤ |d * r₁| + |b * r₂| := abs_sub _ _ _ = |d| * |r₁| + |b| * |r₂| := by simp only [abs_mul] _ ≤ (2 * M) * η + (2 * M) * η := by exact add_le_add (mul_le_mul hcoeff.2.2.2 hr₁ (abs_nonneg r₁) (by positivity)) (mul_le_mul hcoeff.2.1 hr₂ (abs_nonneg r₂) (by positivity)) _ = 4 * M * η := by ring have hynum : |a * r₂ - c * r₁| ≤ 4 * M * η := by calc |a * r₂ - c * r₁| ≤ |a * r₂| + |c * r₁| := abs_sub _ _ _ = |a| * |r₂| + |c| * |r₁| := by simp only [abs_mul] _ ≤ (2 * M) * η + (2 * M) * η := by exact add_le_add (mul_le_mul hcoeff.1 hr₂ (abs_nonneg r₂) (by positivity)) (mul_le_mul hcoeff.2.2.1 hr₁ (abs_nonneg r₁) (by positivity)) _ = 4 * M * η := by ring have hxmul : δ * |x| ≤ 4 * M * η := by calc δ * |x| ≤ |a * d - c * b| * |x| := by gcongr _ = |d * r₁ - b * r₂| := by rw [← abs_mul, hxid] _ ≤ 4 * M * η := hxnum have hymul : δ * |y| ≤ 4 * M * η := by calc δ * |y| ≤ |a * d - c * b| * |y| := by gcongr _ = |a * r₂ - c * r₁| := by rw [← abs_mul, hyid] _ ≤ 4 * M * η := hynum constructor <;> unfold pairwiseSolveFactor <;> rw [div_mul_eq_mul_div] <;> apply (le_div_iff₀ hδ).2 <;> nlinarith [mul_nonneg hM hη] -
selectedTriple_offDiagonal_controltheorem — One separating triple of environments controls both directed off-diagonal transition errors for matrix family, shifts, reference, and candidate over environments E in dimension p. It uses scale, margin, and residual parameters, selected coordinates and their distinctness, environment triple, nonnegative scale and residual with positive margin, bounded shifts and determinant separation, an invertible exact reference, and an approximately diagonal candidate.hypothesesp :ℕE :A :E → SqMatrix ps :E → Fin p → ℝB₀ B :SqMatrix pM δ ε :ℝi j :Fin phij :i ≠ je₀ e₁ e₂ :EhM :0 ≤ Mhδ :0 < δhε :0 ≤ εhscale :ShiftScaleBound s Mhdet :δ ≤ |pairAffineDet s i j e₀ e₁ e₂|hunit :IsUnit B₀.dethexact :ExactCongruence A s B₀happrox :conclusionR :transitionError B₀ Bη :2 * M * entryL2 R ^ 2 + 2 * ε|R i j| ≤ pairwiseSolveFactor M δ * η|R j i| ≤ pairwiseSolveFactor M δ * ηProof (Lean source)
-- Proof route: put `Q = B B₀⁻¹ = I+R`. Subtract the congruence equations at `e₀` -- from those at `e₁,e₂`. The `(i,j)` entries give a 2×2 system in `R i j` and -- `R j i`; `coordinateProductRemainder_le` bounds its nonlinear terms and the two -- off-diagonal residuals contribute `2ε`. Apply `pair_cramer_control`. theorem selectedTriple_offDiagonal_control {p : ℕ} {E : Type*} [Fintype E] [Nonempty E] (A : E → SqMatrix p) (s : E → Fin p → ℝ) (B₀ B : SqMatrix p) {M δ ε : ℝ} (i j : Fin p) (hij : i ≠ j) (e₀ e₁ e₂ : E) (hM : 0 ≤ M) (hδ : 0 < δ) (hε : 0 ≤ ε) (hscale : ShiftScaleBound s M) (hdet : δ ≤ |pairAffineDet s i j e₀ e₁ e₂|) (hunit : IsUnit B₀.det) (hexact : ExactCongruence A s B₀) (happrox : OffDiagonalApproximateCongruence A B ε) : let R := transitionError B₀ B let η := 2 * M * entryL2 R ^ 2 + 2 * ε |R i j| ≤ pairwiseSolveFactor M δ * η ∧ |R j i| ≤ pairwiseSolveFactor M δ * η := by classical dsimp only let Q := transition B₀ B let R := transitionError B₀ B have hQR : Q = 1 + R := by ext u v simp [Q, R, transitionError, Matrix.sub_apply] have hformula (e : E) : (B * A e * B.transpose) i j = R i j * s e j + R j i * s e i + ∑ k, R i k * R j k * s e k := by rw [← transition_diagonal_congruence A s B₀ B hunit hexact e] have hentry : (Q * diagonal (s e) * Q.transpose) i j = ∑ k, Q i k * s e k * Q j k := by simp [Matrix.mul_apply, Matrix.diagonal_apply] change (Q * diagonal (s e) * Q.transpose) i j = _ rw [hentry, hQR] simp only [Matrix.add_apply, Matrix.one_apply] ring_nf repeat rw [Finset.sum_add_distrib] simp only [ite_mul, one_mul, zero_mul, mul_ite, mul_one, mul_zero, Finset.sum_ite_eq, Finset.mem_univ, ↓reduceIte] rw [if_neg hij] have hsum : (∑ k, R i k * s e k * R j k) = ∑ k, R i k * R j k * s e k := by apply Finset.sum_congr rfl intro k hk ring rw [hsum] ring have hlinear (e' e : E) : (s e' j - s e j) * R i j + (s e' i - s e i) * R j i = ((B * A e' * B.transpose) i j - (B * A e * B.transpose) i j) - ∑ k, R i k * R j k * (s e' k - s e k) := by rw [hformula e', hformula e] simp_rw [mul_sub] rw [Finset.sum_sub_distrib] ring let a := s e₁ j - s e₀ j let b := s e₁ i - s e₀ i let c := s e₂ j - s e₀ j let d := s e₂ i - s e₀ i let r₁ := ((B * A e₁ * B.transpose) i j - (B * A e₀ * B.transpose) i j) - ∑ k, R i k * R j k * (s e₁ k - s e₀ k) let r₂ := ((B * A e₂ * B.transpose) i j - (B * A e₀ * B.transpose) i j) - ∑ k, R i k * R j k * (s e₂ k - s e₀ k) have heq₁ : a * R i j + b * R j i = r₁ := by simpa [a, b, r₁] using hlinear e₁ e₀ have heq₂ : c * R i j + d * R j i = r₂ := by simpa [c, d, r₂] using hlinear e₂ e₀ have hcoeff : |a| ≤ 2 * M ∧ |b| ≤ 2 * M ∧ |c| ≤ 2 * M ∧ |d| ≤ 2 * M := by have hdiff (e' e : E) (k : Fin p) : |s e' k - s e k| ≤ 2 * M := by calc |s e' k - s e k| ≤ |s e' k| + |s e k| := abs_sub _ _ _ ≤ M + M := add_le_add (hscale _ _) (hscale _ _) _ = 2 * M := by ring exact ⟨hdiff e₁ e₀ j, hdiff e₁ e₀ i, hdiff e₂ e₀ j, hdiff e₂ e₀ i⟩ have hdet' : δ ≤ |a * d - c * b| := by have heqdet : a * d - c * b = -pairAffineDet s i j e₀ e₁ e₂ := by simp [a, b, c, d, pairAffineDet] ring rw [heqdet, abs_neg] exact hdet have houtput (e' e : E) : |(B * A e' * B.transpose) i j - (B * A e * B.transpose) i j| ≤ 2 * ε := by calc |_ - _| ≤ |(B * A e' * B.transpose) i j| + |(B * A e * B.transpose) i j| := abs_sub _ _ _ ≤ ε + ε := add_le_add (happrox e' i j hij) (happrox e i j hij) _ = 2 * ε := by ring have hr₁ : |r₁| ≤ 2 * M * entryL2 R ^ 2 + 2 * ε := by dsimp [r₁] calc |_ - _| ≤ |(B * A e₁ * B.transpose) i j - (B * A e₀ * B.transpose) i j| + |∑ k, R i k * R j k * (s e₁ k - s e₀ k)| := abs_sub _ _ _ ≤ 2 * ε + 2 * M * entryL2 R ^ 2 := add_le_add (houtput e₁ e₀) (coordinateProductRemainder_le s R hM hscale e₁ e₀ i j) _ = 2 * M * entryL2 R ^ 2 + 2 * ε := by ring have hr₂ : |r₂| ≤ 2 * M * entryL2 R ^ 2 + 2 * ε := by dsimp [r₂] calc |_ - _| ≤ |(B * A e₂ * B.transpose) i j - (B * A e₀ * B.transpose) i j| + |∑ k, R i k * R j k * (s e₂ k - s e₀ k)| := abs_sub _ _ _ ≤ 2 * ε + 2 * M * entryL2 R ^ 2 := add_le_add (houtput e₂ e₀) (coordinateProductRemainder_le s R hM hscale e₂ e₀ i j) _ = 2 * M * entryL2 R ^ 2 + 2 * ε := by ring have hη : 0 ≤ 2 * M * entryL2 R ^ 2 + 2 * ε := by positivity change |R i j| ≤ _ ∧ |R j i| ≤ _ exact pair_cramer_control hM hδ hη hcoeff hdet' heq₁ heq₂ hr₁ hr₂ -
diagonalBranch_controltheorem — Unit-diagonal normalization turns off-diagonal transition control into diagonal control, for reference and candidate matrices in dimension p with invertible reference and both diagonals normalized.hypothesesconclusion|transitionError B₀ B i i| ^ 2≤ ‖B₀‖ ^ 2 * ∑ k ∈ (Finset.univ.erase i), |transitionError B₀ B i k| ^ 2Proof (Lean source)
-- Proof route: `B = (I+R)B₀`; comparing diagonal entries gives -- `R i i = -∑_{k≠i} R i k B₀ k i`, then apply Cauchy--Schwarz. theorem diagonalBranch_control {p : ℕ} (B₀ B : SqMatrix p) (hunit : IsUnit B₀.det) (hdiag₀ : UnitDiagonal B₀) (hdiag : UnitDiagonal B) : ∀ i, |transitionError B₀ B i i| ^ 2 ≤ ‖B₀‖ ^ 2 * ∑ k ∈ (Finset.univ.erase i), |transitionError B₀ B i k| ^ 2 := by classical let R := transitionError B₀ B have hRB : R * B₀ = B - B₀ := by dsimp [R, transitionError, transition] rw [Matrix.sub_mul, Matrix.one_mul] simpa only [Matrix.mul_assoc] using congrArg (fun X : SqMatrix p => X - B₀) (Matrix.nonsing_inv_mul_cancel_right B₀ B hunit) intro i have hentry := congrArg (fun X : SqMatrix p => X i i) hRB simp only [Matrix.mul_apply, Matrix.sub_apply, hdiag i, hdiag₀ i, sub_self] at hentry have hsplit := Finset.sum_erase_add (Finset.univ : Finset (Fin p)) (fun k => R i k * B₀ k i) (Finset.mem_univ i) have heq : R i i = -∑ k ∈ Finset.univ.erase i, R i k * B₀ k i := by rw [← hsplit, hdiag₀ i, mul_one] at hentry linarith have hcolumn : ∑ k ∈ Finset.univ.erase i, |B₀ k i| ^ 2 ≤ ‖B₀‖ ^ 2 := by let e : EuclideanSpace ℝ (Fin p) := toLp 2 (single i 1) have he : ‖e‖ = 1 := by simp [e] have hmul := Matrix.l2_opNorm_mulVec B₀ e rw [he, mul_one] at hmul have hfull : ∑ k, |B₀ k i| ^ 2 ≤ ‖B₀‖ ^ 2 := by have hsquare := (sq_le_sq₀ (norm_nonneg _) (norm_nonneg _)).mpr hmul rw [EuclideanSpace.norm_sq_eq] at hsquare simpa [e, mulVec, dotProduct, sq_abs] using hsquare exact (Finset.sum_le_sum_of_subset_of_nonneg (Finset.erase_subset _ _) (fun _ _ _ => sq_nonneg _)).trans hfull change |R i i| ^ 2 ≤ ‖B₀‖ ^ 2 * ∑ k ∈ Finset.univ.erase i, |R i k| ^ 2 rw [heq, abs_neg, sq_abs] calc (∑ k ∈ Finset.univ.erase i, R i k * B₀ k i) ^ 2 ≤ (∑ k ∈ Finset.univ.erase i, (R i k) ^ 2) * ∑ k ∈ Finset.univ.erase i, (B₀ k i) ^ 2 := Finset.sum_mul_sq_le_sq_mul_sq _ _ _ _ = (∑ k ∈ Finset.univ.erase i, |R i k| ^ 2) * ∑ k ∈ Finset.univ.erase i, |B₀ k i| ^ 2 := by simp only [sq_abs] _ ≤ (∑ k ∈ Finset.univ.erase i, |R i k| ^ 2) * ‖B₀‖ ^ 2 := by exact mul_le_mul_of_nonneg_left hcolumn (Finset.sum_nonneg fun _ _ => sq_nonneg _) _ = ‖B₀‖ ^ 2 * ∑ k ∈ Finset.univ.erase i, |R i k| ^ 2 := by ring -
entryL2_transitionError_letheorem — Uniform off-diagonal control aggregates into a full entrywise transition-error bound for reference and candidate matrices in dimension p, with matrix and entry bounds L,c, positive dimension and nonnegative bounds, an invertible unit-diagonal reference and unit-diagonal candidate, reference norm control, and common off-diagonal control.hypothesesp :ℕB₀ B :SqMatrix pL c :ℝhp :0 < phL :0 ≤ Lhc :0 ≤ chunit :IsUnit B₀.dethdiag₀ :UnitDiagonal B₀hdiag :hB₀ :‖B₀‖ ≤ Lhoff :∀ i jifi ≠ jthen|transitionError B₀ B i j| ≤ cconclusionProof (Lean source)
theorem entryL2_transitionError_le {p : ℕ} (B₀ B : SqMatrix p) {L c : ℝ} (hp : 0 < p) (hL : 0 ≤ L) (hc : 0 ≤ c) (hunit : IsUnit B₀.det) (hdiag₀ : UnitDiagonal B₀) (hdiag : UnitDiagonal B) (hB₀ : ‖B₀‖ ≤ L) (hoff : ∀ i j, i ≠ j → |transitionError B₀ B i j| ≤ c) : entryL2 (transitionError B₀ B) ≤ c * sqrt ((p : ℝ) * (p - 1 : ℕ) * (1 + L ^ 2)) := by classical let R := transitionError B₀ B have hdiagControl := diagonalBranch_control B₀ B hunit hdiag₀ hdiag have hnormsq : ‖B₀‖ ^ 2 ≤ L ^ 2 := (sq_le_sq₀ (norm_nonneg _) hL).mpr hB₀ have hoffSq (i k : Fin p) (hik : i ≠ k) : |R i k| ^ 2 ≤ c ^ 2 := by exact (sq_le_sq₀ (abs_nonneg _) hc).mpr (by simpa [R] using hoff i k hik) have herase (i : Fin p) : ∑ k ∈ Finset.univ.erase i, |R i k| ^ 2 ≤ (p - 1 : ℕ) * c ^ 2 := by calc ∑ k ∈ Finset.univ.erase i, |R i k| ^ 2 ≤ (Finset.univ.erase i).card • c ^ 2 := Finset.sum_le_card_nsmul _ _ _ (fun k hk => hoffSq i k (by simpa [ne_comm] using (Finset.mem_erase.mp hk).1)) _ = (p - 1 : ℕ) * c ^ 2 := by rw [Finset.card_erase_of_mem (Finset.mem_univ i), Finset.card_univ, Fintype.card_fin] norm_num have hrow (i : Fin p) : ∑ k, |R i k| ^ 2 ≤ (1 + L ^ 2) * ∑ k ∈ Finset.univ.erase i, |R i k| ^ 2 := by have hsplit := Finset.sum_erase_add (Finset.univ : Finset (Fin p)) (fun k => |R i k| ^ 2) (Finset.mem_univ i) rw [← hsplit] calc (∑ k ∈ Finset.univ.erase i, |R i k| ^ 2) + |R i i| ^ 2 ≤ (∑ k ∈ Finset.univ.erase i, |R i k| ^ 2) + ‖B₀‖ ^ 2 * ∑ k ∈ Finset.univ.erase i, |R i k| ^ 2 := by gcongr simpa [R] using hdiagControl i _ ≤ (∑ k ∈ Finset.univ.erase i, |R i k| ^ 2) + L ^ 2 * ∑ k ∈ Finset.univ.erase i, |R i k| ^ 2 := by gcongr _ = (1 + L ^ 2) * ∑ k ∈ Finset.univ.erase i, |R i k| ^ 2 := by ring have hsum : ∑ i, ∑ k, |R i k| ^ 2 ≤ (p : ℝ) * (p - 1 : ℕ) * c ^ 2 * (1 + L ^ 2) := by calc ∑ i, ∑ k, |R i k| ^ 2 ≤ ∑ i, (1 + L ^ 2) * ∑ k ∈ Finset.univ.erase i, |R i k| ^ 2 := by gcongr with i exact hrow i _ ≤ ∑ _i : Fin p, (1 + L ^ 2) * ((p - 1 : ℕ) * c ^ 2) := by gcongr with i exact herase i _ = (p : ℝ) * (p - 1 : ℕ) * c ^ 2 * (1 + L ^ 2) := by simp [Finset.card_univ, Fintype.card_fin] ring rw [entryL2_eq_sqrt, Real.sqrt_le_iff] constructor · positivity · calc ∑ i, ∑ j, |R i j| ^ 2 ≤ (p : ℝ) * (p - 1 : ℕ) * c ^ 2 * (1 + L ^ 2) := hsum _ = (c * sqrt ((p : ℝ) * (p - 1 : ℕ) * (1 + L ^ 2))) ^ 2 := by rw [mul_pow, Real.sq_sqrt] · ring · positivity
SmallParameter 1 core · 2 supporting This module proves the openness step for the transformed invariant and packages all algebraic, normalization, invertibility, cycle-product, and nonnegativity constraints into one arbitrarily-small nonzero parameter choic ★ exists_small_admissible_parameter
Selecting a simultaneous small deformation parameter
This module proves the openness step for the transformed invariant and packages all algebraic, normalization, invertibility, cycle-product, and nonnegativity constraints into one arbitrarily-small nonzero parameter choice.
theorem exists_small_admissible_parameter reviewed
⚑ flagged
Causalean.Discovery.LinearDisentanglement.SimultaneousCongruence
Every positive neighborhood contains a nontrivial admissible ambiguity deformation, showing the nonidentification is genuinely local. For dimension d, environment type E, reference diagonalizer B, invariant Ω, and selected coordinates, this uses distinctness, unit diagonal, invertibility, cycle admissibility, and positive definiteness, shift family s, line normal and offset u,v,c, nonzero normal and nonnegative shifts, and positive radius r.
Formal statement
hypotheses
d :
ℕ
E :
Type*
B Ω :
SqMatrix d
i j :
Fin d
hij :
i ≠ j
hBdiag :
hBunit :
IsUnit B.det
hcycle :
PairCycleAdmissible B i j
hΩ :
Ω.PosDef
s :
E → Fin d → ℝ
u v c :
ℝ
hnormal :
u ≠ 0 ∨ v ≠ 0
hs :
∀ e k, 0 ≤ s e k
r :
ℝ
hr :
0 < r
conclusion
∃ t : ℝ,
0 < |t|
|t| < r
firstNormalizationDenom B i j v t ≠ 0
secondNormalizationDenom B i j u t ≠ 0
1 - t ^ 2 * u * v ≠ 0
IsUnit (normalizedPairDeformation B i j u v t).det
IsUnit (deformedDiagonalizer B i j u v t).det
UnitDiagonal (deformedDiagonalizer B i j u v t)
PairCycleAdmissible (deformedDiagonalizer B i j u v t) i j
deformedDiagonalizer B i j u v t ≠ B
(deformedInvariant B Ω i j u v c t).PosDef
Proof (Lean source)
theorem exists_small_admissible_parameter {d : ℕ} {E : Type*}
(B Ω : SqMatrix d) {i j : Fin d}
(hij : i ≠ j) (hBdiag : UnitDiagonal B) (hBunit : IsUnit B.det)
(hcycle : PairCycleAdmissible B i j) (hΩ : Ω.PosDef)
(s : E → Fin d → ℝ) (u v c : ℝ) (hnormal : u ≠ 0 ∨ v ≠ 0)
(hs : ∀ e k, 0 ≤ s e k) {r : ℝ} (hr : 0 < r) :
∃ t : ℝ,
0 < |t| ∧ |t| < r ∧
firstNormalizationDenom B i j v t ≠ 0 ∧
secondNormalizationDenom B i j u t ≠ 0 ∧
1 - t ^ 2 * u * v ≠ 0 ∧
IsUnit (normalizedPairDeformation B i j u v t).det ∧
IsUnit (deformedDiagonalizer B i j u v t).det ∧
UnitDiagonal (deformedDiagonalizer B i j u v t) ∧
PairCycleAdmissible (deformedDiagonalizer B i j u v t) i j ∧
deformedDiagonalizer B i j u v t ≠ B ∧
(deformedInvariant B Ω i j u v c t).PosDef ∧
∀ e k, 0 ≤ deformedShift B i j u v t (s e) k := by
rcases exists_deformedInvariant_posDef_radius B Ω hΩ
u v c with ⟨ρp, hρp, hp⟩
rcases exists_algebraic_admissibility_radius B i j u v with
⟨ρa, hρa, ha⟩
let δ := min r (min ρp ρa)
let t := δ / 2
have hδ : 0 < δ := by
exact lt_min hr (lt_min hρp hρa)
have ht_abs : |t| = δ / 2 := by
rw [abs_of_pos]
exact div_pos hδ (by norm_num)
have ht0 : 0 < |t| := by rw [ht_abs]; positivity
have htr : |t| < r := by
rw [ht_abs]
have hδr : δ ≤ r := min_le_left _ _
linarith
have htp : |t| < ρp := by
rw [ht_abs]
have hδp : δ ≤ ρp := (min_le_right r _).trans (min_le_left _ _)
linarith
have hta : |t| < ρa := by
rw [ht_abs]
have hδa : δ ≤ ρa := (min_le_right r _).trans (min_le_right _ _)
linarith
rcases ha t hta with ⟨hfirst, hsecond, hdet⟩
have hTunit : IsUnit (normalizedPairDeformation B i j u v t).det :=
normalizedPairDeformation_isUnit_det B hij hfirst hsecond hdet
have hB'unit : IsUnit (deformedDiagonalizer B i j u v t).det := by
rw [deformedDiagonalizer, Matrix.det_mul]
exact hTunit.mul hBunit
have hdiag : UnitDiagonal (deformedDiagonalizer B i j u v t) :=
deformedDiagonalizer_unitDiagonal B hij hBdiag hfirst hsecond
have hcycle' : PairCycleAdmissible
(deformedDiagonalizer B i j u v t) i j :=
deformedDiagonalizer_pairCycleAdmissible B hij hBdiag hcycle
hfirst hsecond hdet
have htne : t ≠ 0 := abs_pos.mp ht0
have hne : deformedDiagonalizer B i j u v t ≠ B :=
deformedDiagonalizer_ne B hij hBunit hnormal htne hfirst hsecond
have hpos : (deformedInvariant B Ω i j u v c t).PosDef :=
hp t htp
have hshift : ∀ e k, 0 ≤ deformedShift B i j u v t (s e) k := by
intro e
exact deformedShift_nonnegative B hij u v t (s e) (hs e)
exact ⟨t, ht0, htr, hfirst, hsecond, hdet, hTunit, hB'unit,
hdiag, hcycle', hne, hpos, hshift⟩
2 supporting declarations (lemmas, instances)
-
exists_deformedInvariant_posDef_radiustheorem — When the original invariant is positive definite, some positive radius keeps every transformed invariant positive definite.hypothesesconclusion∃ ρ > 0, ∀ t : ℝ, |t| < ρ → (deformedInvariant B Ω i j u v c t).PosDefProof (Lean source)
theorem exists_deformedInvariant_posDef_radius {d : ℕ} (B Ω : SqMatrix d) {i j : Fin d} (hΩ : Ω.PosDef) (u v c : ℝ) : ∃ ρ > 0, ∀ t : ℝ, |t| < ρ → (deformedInvariant B Ω i j u v c t).PosDef := by have heventually : ∀ᶠ t in nhds 0, (deformedInvariant B Ω i j u v c t).PosDef := posDef_eventually_of_continuousAt (fun t ↦ deformedInvariant B Ω i j u v c t) (continuousAt_deformedInvariant B Ω i j u v c) (by simpa using hΩ) (deformedInvariant_isHermitian B Ω i j hΩ u v c) rcases Metric.mem_nhds_iff.mp heventually with ⟨ρ, hρ, hball⟩ refine ⟨ρ, hρ, fun t ht ↦ hball ?_⟩ simpa [Metric.mem_ball, Real.dist_eq] using ht -
exists_algebraic_admissibility_radiustheorem — Some positive radius makes both row-normalization denominators and the selected shear determinant nonzero.hypothesesconclusion∃ ρ > 0,∀ t : ℝ,|t| < ρ → firstNormalizationDenom B i j v t ≠ 0 ∧secondNormalizationDenom B i j u t ≠ 0 ∧1 - t ^ 2 * u * v ≠ 0Proof (Lean source)
theorem exists_algebraic_admissibility_radius {d : ℕ} (B : SqMatrix d) (i j : Fin d) (u v : ℝ) : ∃ ρ > 0, ∀ t : ℝ, |t| < ρ → firstNormalizationDenom B i j v t ≠ 0 ∧ secondNormalizationDenom B i j u t ≠ 0 ∧ 1 - t ^ 2 * u * v ≠ 0 := by have hfirst : ∀ᶠ t in nhds 0, firstNormalizationDenom B i j v t ≠ 0 := by apply ContinuousAt.eventually_ne · unfold firstNormalizationDenom fun_prop · simp [firstNormalizationDenom] have hsecond : ∀ᶠ t in nhds 0, secondNormalizationDenom B i j u t ≠ 0 := by apply ContinuousAt.eventually_ne · unfold secondNormalizationDenom fun_prop · simp [secondNormalizationDenom] have hdet : ∀ᶠ t in nhds 0, 1 - t ^ 2 * u * v ≠ 0 := by apply ContinuousAt.eventually_ne · fun_prop · norm_num have hall : ∀ᶠ t in nhds 0, firstNormalizationDenom B i j v t ≠ 0 ∧ secondNormalizationDenom B i j u t ≠ 0 ∧ 1 - t ^ 2 * u * v ≠ 0 := by filter_upwards [hfirst, hsecond, hdet] with t ht1 ht2 ht3 exact ⟨ht1, ht2, ht3⟩ rcases Metric.mem_nhds_iff.mp hall with ⟨ρ, hρ, hball⟩ refine ⟨ρ, hρ, fun t ht ↦ hball ?_⟩ simpa [Metric.mem_ball, Real.dist_eq] using ht
Stability 1 core · 4 supporting This module aggregates the pair-dependent two-coordinate estimates, uses an explicit small-residual threshold and ordinary local neighborhood to select the identity branch, converts entrywise L² control to Euclidean oper ★ opNorm_sub_le_condition_specialization
Local operator-norm stability from pairwise affine separation
This module aggregates the pair-dependent two-coordinate estimates, uses an explicit small-residual threshold and ordinary local neighborhood to select the identity branch, converts entrywise L² control to Euclidean operator norm, and specializes the result to a determinant/condition-number envelope.
theorem opNorm_sub_le_condition_specialization reviewed
⚑ flagged
Causalean.Discovery.LinearDisentanglement.SimultaneousCongruence
The determinant-condition envelope yields the advertised local operator-norm stability rate, replacing an abstract matrix scale by its explicit condition root. For matrix family, shifts, reference, and candidate over environments E in dimension p, with scale, margin, condition, and residual parameters, this uses positive dimension, scale, and margin with condition at least one, bounded separated shifts, normalized matrices and a conditioned reference, exact and approximate feasibility, nonnegative residual, and the small-residual and local-neighborhood conditions.
Formal statement
hypotheses
p :
ℕ
E :
A :
E → SqMatrix p
s :
E → Fin p → ℝ
B₀ B :
SqMatrix p
M γ κ ε :
ℝ
hp :
0 < p
hM :
0 < M
hγ :
0 < γ
hκ :
1 ≤ κ
hscale :
ShiftScaleBound s M
hsep :
hdiag₀ :
UnitDiagonal B₀
hdiag :
hcond :
DetConditionEnvelope κ B₀
hexact :
ExactCongruence A s B₀
hε :
0 ≤ ε
happrox :
hsmall :
ε ≤ pairwiseResidualRadius p M γ (conditionRoot p κ)
hlocal :
conclusion
‖B - B₀‖
≤ 16 * (6 * M / γ) * sqrt ((p : ℝ) * (p - 1 : ℕ) * (1 + conditionRoot p κ ^ 2)) * conditionRoot p κ ^ 3 * ε
Proof (Lean source)
theorem opNorm_sub_le_condition_specialization {p : ℕ} {E : Type*}
[Fintype E] [Nonempty E]
(A : E → SqMatrix p) (s : E → Fin p → ℝ) (B₀ B : SqMatrix p)
{M γ κ ε : ℝ}
(hp : 0 < p) (hM : 0 < M) (hγ : 0 < γ) (hκ : 1 ≤ κ)
(hscale : ShiftScaleBound s M) (hsep : PairwiseAffineSeparated s γ)
(hdiag₀ : UnitDiagonal B₀) (hdiag : UnitDiagonal B)
(hcond : DetConditionEnvelope κ B₀)
(hexact : ExactCongruence A s B₀)
(hε : 0 ≤ ε) (happrox : OffDiagonalApproximateCongruence A B ε)
(hsmall : ε ≤ pairwiseResidualRadius p M γ (conditionRoot p κ))
(hlocal : InReferenceNeighborhood
(pairwiseLocalRadius p M γ (conditionRoot p κ) κ) B₀ B) :
‖B - B₀‖ ≤
16 * (6 * M / γ) *
sqrt ((p : ℝ) * (p - 1 : ℕ) *
(1 + conditionRoot p κ ^ 2)) *
conditionRoot p κ ^ 3 * ε := by
have hL : 1 ≤ conditionRoot p κ := one_le_conditionRoot hp hκ
have hB₀ : ‖B₀‖ ≤ conditionRoot p κ :=
opNorm_le_conditionRoot B₀ hp hcond
have hinv : ‖B₀⁻¹‖ ≤ κ :=
invOpNorm_le_conditionEnvelope B₀ hp hdiag₀ hcond
have hJ : 0 < κ := lt_of_lt_of_le zero_lt_one hκ
have h := opNorm_sub_le_of_pairwise_affine (J := κ) A s B₀ B hp hM hγ hL hJ
hscale hsep hcond.1 hexact hdiag₀ hdiag hB₀ hinv hε hsmall happrox hlocal
calc
‖B - B₀‖ ≤ pairwiseStabilityConstant p M γ (conditionRoot p κ) * ε := h
_ = 16 * (6 * M / γ) *
sqrt ((p : ℝ) * (p - 1 : ℕ) * (1 + conditionRoot p κ ^ 2)) *
conditionRoot p κ ^ 3 * ε := by
unfold pairwiseStabilityConstant pairwiseAggregateFactor pairwiseSolveFactor
ring
4 supporting declarations (lemmas, instances)
-
opNorm_le_entryL2theorem — Operator norm is bounded by entrywise Euclidean size, allowing aggregate control of matrix error R in dimension p to imply worst-direction control. -
sub_eq_transitionError_multheorem — Candidate-reference error factors through transition error, converting relative error back to the original scale for reference and candidate matrices in dimension p when the reference is invertible.hypothesesconclusionB - B₀ = transitionError B₀ B * B₀Proof (Lean source)
theorem sub_eq_transitionError_mul {p : ℕ} (B₀ B : SqMatrix p) (hunit : IsUnit B₀.det) : B - B₀ = transitionError B₀ B * B₀ := by rw [transitionError, Matrix.sub_mul, Matrix.one_mul, transition] rw [Matrix.nonsing_inv_mul_cancel_right B₀ B hunit] -
opNorm_sub_le_of_pairwise_affine_in_identity_branchtheorem — Local pairwise-affine simultaneous-congruence stability. For positive dimension, shift scale, and affine margin, a matrix scale at least one, bounded pairwise-separated shifts, an exact invertible unit-diagonal reference, a unit-diagonal candidate, a reference operator norm at most the matrix scale, nonnegative off-diagonal residual tolerance, off-diagonal approximate feasibility, and the explicit local identity-branch condition, the candidate-reference Euclidean operator distance is linear in the residual.hypothesesp :ℕE :A :E → SqMatrix ps :E → Fin p → ℝB₀ B :SqMatrix pM δ L ε :ℝhp :0 < phM :0 < Mhδ :0 < δhL :1 ≤ Lhscale :ShiftScaleBound s Mhsep :hunit :IsUnit B₀.dethexact :ExactCongruence A s B₀hdiag₀ :UnitDiagonal B₀hdiag :hB₀ :‖B₀‖ ≤ Lhε :0 ≤ εhapprox :hbranch :InIdentityBranch M δ L B₀ Bconclusion‖B - B₀‖ ≤ pairwiseStabilityConstant p M δ L * εProof (Lean source)
-- Proof route: `pairwise_offDiagonal_control` and `entryL2_transitionError_le` give -- `u ≤ K (2 M u² + 2ε)`. The second identity-branch inequality absorbs the quadratic -- term, yielding `u ≤ 4Kε`. Factor `B-B₀ = R B₀`, use -- `‖R‖op ≤ entryL2 R`, and weaken `4KL` to the displayed `16KL³` using `1 ≤ L`. theorem opNorm_sub_le_of_pairwise_affine_in_identity_branch {p : ℕ} {E : Type*} [Fintype E] [Nonempty E] (A : E → SqMatrix p) (s : E → Fin p → ℝ) (B₀ B : SqMatrix p) {M δ L ε : ℝ} (hp : 0 < p) (hM : 0 < M) (hδ : 0 < δ) (hL : 1 ≤ L) (hscale : ShiftScaleBound s M) (hsep : PairwiseAffineSeparated s δ) (hunit : IsUnit B₀.det) (hexact : ExactCongruence A s B₀) (hdiag₀ : UnitDiagonal B₀) (hdiag : UnitDiagonal B) (hB₀ : ‖B₀‖ ≤ L) (hε : 0 ≤ ε) (happrox : OffDiagonalApproximateCongruence A B ε) (hbranch : InIdentityBranch M δ L B₀ B) : ‖B - B₀‖ ≤ pairwiseStabilityConstant p M δ L * ε := by let R := transitionError B₀ B let K := pairwiseAggregateFactor p M δ L have hL0 : 0 ≤ L := le_trans (by norm_num) hL have hK0 : 0 ≤ K := by dsimp [K, pairwiseAggregateFactor, pairwiseSolveFactor] positivity have hu0 : 0 ≤ entryL2 R := entryL2_nonneg R have hc0 : 0 ≤ pairwiseSolveFactor M δ * (2 * M * entryL2 R ^ 2 + 2 * ε) := by unfold pairwiseSolveFactor positivity have hoff : ∀ i j, i ≠ j → |R i j| ≤ pairwiseSolveFactor M δ * (2 * M * entryL2 R ^ 2 + 2 * ε) := by simpa [R] using pairwise_offDiagonal_control A s B₀ B hM.le hδ hε hscale hsep hunit hexact happrox have hu := entryL2_transitionError_le B₀ B hp hL0 hc0 hunit hdiag₀ hdiag hB₀ hoff have huK : entryL2 R ≤ K * (2 * M * entryL2 R ^ 2 + 2 * ε) := by change entryL2 R ≤ pairwiseSolveFactor M δ * (2 * M * entryL2 R ^ 2 + 2 * ε) * sqrt ((p : ℝ) * (p - 1 : ℕ) * (1 + L ^ 2)) at hu calc entryL2 R ≤ pairwiseSolveFactor M δ * (2 * M * entryL2 R ^ 2 + 2 * ε) * sqrt ((p : ℝ) * (p - 1 : ℕ) * (1 + L ^ 2)) := hu _ = K * (2 * M * entryL2 R ^ 2 + 2 * ε) := by dsimp [K, pairwiseAggregateFactor] ring have hbranch' : 2 * K * M * entryL2 R ≤ 1 / 2 := by simpa [R, K, InIdentityBranch] using hbranch.2 have hquad : K * (2 * M * entryL2 R ^ 2) ≤ entryL2 R / 2 := by nlinarith [mul_nonneg hu0 (sub_nonneg.mpr hbranch')] have huLinear : entryL2 R ≤ 4 * K * ε := by nlinarith rw [sub_eq_transitionError_mul B₀ B hunit] calc ‖transitionError B₀ B * B₀‖ ≤ ‖transitionError B₀ B‖ * ‖B₀‖ := norm_mul_le _ _ _ ≤ entryL2 R * L := by exact mul_le_mul (by simpa [R] using opNorm_le_entryL2 R) hB₀ (norm_nonneg _) hu0 _ ≤ (4 * K * ε) * L := by gcongr _ ≤ pairwiseStabilityConstant p M δ L * ε := by unfold pairwiseStabilityConstant dsimp [K] have hL3 : 1 ≤ L ^ 3 := one_le_pow₀ hL have hcoef : 4 * L ≤ 16 * L ^ 3 := by nlinarith calc (4 * pairwiseAggregateFactor p M δ L * ε) * L = (pairwiseAggregateFactor p M δ L * ε) * (4 * L) := by ring _ ≤ (pairwiseAggregateFactor p M δ L * ε) * (16 * L ^ 3) := mul_le_mul_of_nonneg_left hcoef (mul_nonneg hK0 hε) _ = 16 * pairwiseAggregateFactor p M δ L * L ^ 3 * ε := by ring -
opNorm_sub_le_of_pairwise_affinetheorem — Small-residual local pairwise-affine simultaneous-congruence stability. For positive dimension, shift scale, affine margin, matrix scale, and inverse envelope, bounded pairwise-separated shifts, an exact invertible unit-diagonal reference, a unit-diagonal candidate, a reference operator norm at most the matrix scale, a reference inverse bound, nonnegative off-diagonal residual below the explicit threshold, approximate feasibility, and membership in the explicit entrywise-L² neighborhood of the reference, the candidate-reference Euclidean operator distance is linear in the residual.hypothesesp :ℕE :A :E → SqMatrix ps :E → Fin p → ℝB₀ B :SqMatrix pM δ L J ε :ℝhp :0 < phM :0 < Mhδ :0 < δhL :1 ≤ LhJ :0 < Jhscale :ShiftScaleBound s Mhsep :hunit :IsUnit B₀.dethexact :ExactCongruence A s B₀hdiag₀ :UnitDiagonal B₀hdiag :hB₀ :‖B₀‖ ≤ Lhinv :‖B₀⁻¹‖ ≤ Jhε :0 ≤ εhsmall :ε ≤ pairwiseResidualRadius p M δ Lhapprox :hlocal :InReferenceNeighborhood (pairwiseLocalRadius p M δ L J) B₀ Bconclusion‖B - B₀‖ ≤ pairwiseStabilityConstant p M δ L * εProof (Lean source)
theorem opNorm_sub_le_of_pairwise_affine {p : ℕ} {E : Type*} [Fintype E] [Nonempty E] (A : E → SqMatrix p) (s : E → Fin p → ℝ) (B₀ B : SqMatrix p) {M δ L J ε : ℝ} (hp : 0 < p) (hM : 0 < M) (hδ : 0 < δ) (hL : 1 ≤ L) (hJ : 0 < J) (hscale : ShiftScaleBound s M) (hsep : PairwiseAffineSeparated s δ) (hunit : IsUnit B₀.det) (hexact : ExactCongruence A s B₀) (hdiag₀ : UnitDiagonal B₀) (hdiag : UnitDiagonal B) (hB₀ : ‖B₀‖ ≤ L) (hinv : ‖B₀⁻¹‖ ≤ J) (hε : 0 ≤ ε) (hsmall : ε ≤ pairwiseResidualRadius p M δ L) (happrox : OffDiagonalApproximateCongruence A B ε) (hlocal : InReferenceNeighborhood (pairwiseLocalRadius p M δ L J) B₀ B) : ‖B - B₀‖ ≤ pairwiseStabilityConstant p M δ L * ε := by have hbranch := inIdentityBranch_of_small_residual A s B₀ B hp hM hδ hL hJ hscale hsep hunit hexact hdiag₀ hdiag hB₀ hinv hε hsmall happrox hlocal exact opNorm_sub_le_of_pairwise_affine_in_identity_branch A s B₀ B hp hM hδ hL hscale hsep hunit hexact hdiag₀ hdiag hB₀ hε happrox hbranch