OAI/Dynamics/SmoothObstruction/MinorTransfer.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SmoothObstruction.EuclideanSplitting.projected_nonleading_minor line 14

   Source documentation

   Actual endpoint-projected nonleading maximal minors on unit starting columns. The inter-group conditioning is paid only by the finite gauge.

   theorem projected_nonleading_minor
       (U V : ℕ → Matrix (Fin d) (Fin d) ℝ) (lam : Fin d → ℝ)
       (hUV : ∀ t,U t*V t=1) (hVU : ∀ t,V t*U t=1)
       (S : Finset (Fin d)) {s t : ℕ} (hst : s≤t) {γ g K C : ℝ}
       (hg : 0≤g) (hK : 0≤K) (hC : 0≤C)
       (hfast : ∀ j∈S,γ+g≤lam j) (hslow : ∀ j∉S,lam j≤γ-g)
       (hU : ‖U t‖≤Real.exp K) (hV : ‖V s‖≤Real.exp K)
       (hpoly : ∀ A : EuclideanSpace ℝ (Fin d) →L[ℝ] EuclideanSpace ℝ (Fin d),
         ‖exterior S.card A‖≤C*(max 1 ‖A‖)^S.card)
       (W : Submodule ℝ (EuclideanSpace ℝ (Fin d)))
       (b : OrthonormalBasis (Fin d) ℝ (EuclideanSpace ℝ (Fin d)))
       (r : powersetCard (Fin d) S.card)
   …

2. theorem OAI.SmoothObstruction.EuclideanSplitting.fast_minor_volume_lower line 63

   Source documentation

   Actual fast determinant-line bound for arbitrary starting vectors in the fast group. This permits projection of a common orthonormal frame onto the actual group without a polar-decomposition choice of bases.

   theorem fast_minor_volume_lower
       (U V : ℕ → Matrix (Fin d) (Fin d) ℝ) (lam : Fin d → ℝ)
       (hUV : ∀ t,U t*V t=1) (hVU : ∀ t,V t*U t=1)
       (s t p : ℕ) (q : powersetCard (Fin d) p)
       (W : Submodule ℝ (EuclideanSpace ℝ (Fin d)))
       (hdim : Module.finrank ℝ W=p)
       (hclose : ‖(groupSpace (U t) (V t) (hUV t) (hVU t) q.val).starProjection-W.starProjection‖≤1/2)
       (b : OrthonormalBasis (Fin d) ℝ (EuclideanSpace ℝ (Fin d)))
       (r : powersetCard (Fin d) p)
       (hcoords : ∀ x∈W,∀ j∉r,b.repr x j=0)
       (w : Fin p → EuclideanSpace ℝ (Fin d))
       (hw : ∀ i,w i∈groupSpace (U s) (V s) (hUV s) (hVU s) q.val)
   …

   Mentions: OAI.SmoothObstruction.EuclideanSplitting.groupSpace

3. lemma OAI.SmoothObstruction.ExteriorStability.projected_frame_distance line 153
4. theorem OAI.SmoothObstruction.ExteriorStability.exists_common_frame_wedge_control line 169

   Source documentation

   One dimension-dependent uniform constant controls projected common frames. This bypasses choosing a continuously varying orthonormal basis: project the reference columns and use their determinant volume directly.

   theorem exists_common_frame_wedge_control (p : ℕ) :
       ∃ L : ℝ,1≤L ∧ ∀ (F G : Submodule ℝ E) (w : Fin p → E)
         (δ : ℝ), (∀ i,w i∈G) → (∀ i,‖w i‖≤1) → 0≤δ →
         ‖F.starProjection-G.starProjection‖≤δ →
         ‖exteriorPower.ιMulti ℝ p (fun i => F.starProjection (w i))-
           exteriorPower.ιMulti ℝ p w‖≤L*δ := by
   …

5. lemma OAI.SmoothObstruction.ExteriorStability.projected_orthonormal_volume_lower line 187
6. lemma OAI.SmoothObstruction.ExteriorStability.projectedMinor_column_error line 200

   Source documentation

   Column replacement is paid against the TRUE exterior norm of the old propagator, hence it is valid even if the determinant line contracts.

   lemma projectedMinor_column_error (b : OrthonormalBasis ι ℝ E) (p : ℕ)
       (r : powersetCard ι p) (A : E →L[ℝ] E) (v w : Fin p → E)
       {ε : ℝ} (hε : ‖exteriorPower.ιMulti ℝ p v-exteriorPower.ιMulti ℝ p w‖≤ε) :
       |projectedMinor b p r A v-projectedMinor b p r A w|≤‖exterior p A‖*ε := by
   …

   Mentions: OAI.SmoothObstruction.ExteriorStability.projectedMinor, OAI.SmoothObstruction.ExteriorStability.exterior

7. theorem OAI.SmoothObstruction.EuclideanSplitting.old_fast_minor_separation line 217

   Source documentation

   Actual old endpoint minors have the relative fast/slow separation needed for switching. Neither leading lower bounds nor suppressed minor bounds are hypotheses: both are derived from the finite gauge and endpoint geometry.

   theorem old_fast_minor_separation
       (U V : ℕ → Matrix (Fin d) (Fin d) ℝ) (lam : Fin d → ℝ)
       (hUV : ∀ t,U t*V t=1) (hVU : ∀ t,V t*U t=1)
       (S : Finset (Fin d)) {s t : ℕ} (hst : s≤t) {γ g K C : ℝ}
       (hg : 0≤g) (hK : 0≤K) (hC : 0≤C)
       (hfast : ∀ j∈S,γ+g≤lam j) (hslow : ∀ j∉S,lam j≤γ-g)
       (hUs : ‖U s‖≤Real.exp K) (hUt : ‖U t‖≤Real.exp K)
       (hVs : ‖V s‖≤Real.exp K) (hVt : ‖V t‖≤Real.exp K)
       (hpoly : ∀ A : EuclideanSpace ℝ (Fin d) →L[ℝ] EuclideanSpace ℝ (Fin d),
         ‖exterior S.card A‖≤C*(max 1 ‖A‖)^S.card)
       (W : Submodule ℝ (EuclideanSpace ℝ (Fin d)))
       (hdim : Module.finrank ℝ W=S.card)
   …

8. def OAI.SmoothObstruction.ExteriorStability.frameWedgeConstant line 272
9. lemma OAI.SmoothObstruction.ExteriorStability.one_le_frameWedgeConstant line 275
10. lemma OAI.SmoothObstruction.ExteriorStability.frameWedgeConstant_bound line 278
11. theorem OAI.SmoothObstruction.EuclideanSplitting.common_fast_minor_lower line 295

    Source documentation

    A common-bin orthonormal reference frame has a nonzero leading minor at the TRUE sum-rate scale. The proof projects its columns onto the actual fast space and estimates their wedge; it requires no continuous choice of Lyapunov bases or unproved orthonormal basis alignment.

    theorem common_fast_minor_lower
        (U V : ℕ → Matrix (Fin d) (Fin d) ℝ) (lam : Fin d → ℝ)
        (hUV : ∀ t,U t*V t=1) (hVU : ∀ t,V t*U t=1)
        (S : Finset (Fin d)) {s t : ℕ} (hst : s≤t) {γ g K C δ : ℝ}
        (hg : 0≤g) (hK : 0≤K) (hC : 0≤C) (hδ : 0≤δ)
        (hfast : ∀ j∈S,γ+g≤lam j) (hslow : ∀ j∉S,lam j≤γ-g)
        (hUs : ‖U s‖≤Real.exp K) (hUt : ‖U t‖≤Real.exp K)
        (hVs : ‖V s‖≤Real.exp K) (hVt : ‖V t‖≤Real.exp K)
        (hpoly : ∀ A : EuclideanSpace ℝ (Fin d) →L[ℝ] EuclideanSpace ℝ (Fin d),
          ‖exterior S.card A‖≤C*(max 1 ‖A‖)^S.card)
        (W G : Submodule ℝ (EuclideanSpace ℝ (Fin d)))
        (hdim : Module.finrank ℝ W=S.card)
    …

12. def OAI.SmoothObstruction.ExteriorStability.unitWedgeConstant line 376
13. lemma OAI.SmoothObstruction.ExteriorStability.one_le_unitWedgeConstant line 379
14. lemma OAI.SmoothObstruction.ExteriorStability.unit_wedge_difference line 381
15. lemma OAI.SmoothObstruction.ExteriorStability.mixed_projected_wedge_difference line 391

    Source documentation

    The common product frame may mix both groups. Each column is projected onto its OWN actual group; one uniform wedge constant still suffices.

    lemma mixed_projected_wedge_difference (p : ℕ) (F G : Fin p → Submodule ℝ E)
        (w : Fin p → E) (hw : ∀ i,w i∈G i) (hnorm : ∀ i,‖w i‖≤1)
        {δ : ℝ} (hδ : 0≤δ) (hclose : ∀ i,‖(F i).starProjection-(G i).starProjection‖≤δ) :
        ‖exteriorPower.ιMulti ℝ p (fun i => (F i).starProjection (w i))-
          exteriorPower.ιMulti ℝ p w‖≤unitWedgeConstant (E:=E) p*δ := by
    …

    Mentions: OAI.SmoothObstruction.ExteriorStability.unitWedgeConstant

16. theorem OAI.SmoothObstruction.EuclideanSplitting.common_nonleading_minor line 420

    Source documentation

    Every nonleading minor in the common starting product frame has the true relative gap term plus a controlled common-subspace replacement term. No determinant-line rate is assumed nonnegative.

    theorem common_nonleading_minor
        (U V : ℕ → Matrix (Fin d) (Fin d) ℝ) (lam : Fin d → ℝ)
        (hUV : ∀ t,U t*V t=1) (hVU : ∀ t,V t*U t=1)
        (S : Finset (Fin d)) {s t : ℕ} (hst : s≤t) {γ g K C δ : ℝ}
        (hg : 0≤g) (hK : 0≤K) (hC : 0≤C) (hδ : 0≤δ)
        (hfast : ∀ j∈S,γ+g≤lam j) (hslow : ∀ j∉S,lam j≤γ-g)
        (hUt : ‖U t‖≤Real.exp K) (hVs : ‖V s‖≤Real.exp K)
        (hpoly : ∀ A : EuclideanSpace ℝ (Fin d) →L[ℝ] EuclideanSpace ℝ (Fin d),
          ‖exterior S.card A‖≤C*(max 1 ‖A‖)^S.card)
        (W : Submodule ℝ (EuclideanSpace ℝ (Fin d)))
        (b : OrthonormalBasis (Fin d) ℝ (EuclideanSpace ℝ (Fin d)))
        (r : powersetCard (Fin d) S.card)
    …

17. theorem OAI.SmoothObstruction.EuclideanSplitting.common_minor_separation line 506

    Source documentation

    Genuine common-frame minors: the old leading minor is nonzero and every mixed minor has a relative bound obtained from the actual gauge products. All smallness requirements refer to subspace distances, not to conclusions about minors. Rates may be negative and no uniform determinant floor is used.

    theorem common_minor_separation
        (U V : ℕ → Matrix (Fin d) (Fin d) ℝ) (lam : Fin d → ℝ)
        (hUV : ∀ t,U t*V t=1) (hVU : ∀ t,V t*U t=1)
        (S : Finset (Fin d)) {s t : ℕ} (hst : s≤t) {γ g K C δ : ℝ}
        (hg : 0≤g) (hK : 0≤K) (hC : 0≤C) (hδ : 0≤δ)
        (hfast : ∀ j∈S,γ+g≤lam j) (hslow : ∀ j∉S,lam j≤γ-g)
        (hUs : ‖U s‖≤Real.exp K) (hUt : ‖U t‖≤Real.exp K)
        (hVs : ‖V s‖≤Real.exp K) (hVt : ‖V t‖≤Real.exp K)
        (hpoly : ∀ A : EuclideanSpace ℝ (Fin d) →L[ℝ] EuclideanSpace ℝ (Fin d),
          ‖exterior S.card A‖≤C*(max 1 ‖A‖)^S.card)
        (W G : Submodule ℝ (EuclideanSpace ℝ (Fin d)))
        (hdim : Module.finrank ℝ W=S.card)
    …

18. theorem OAI.SmoothObstruction.ExteriorStability.relative_projected_minor line 575

    Source documentation

    Relative transfer of the actual signed projected minor, even when its leading determinant tends to zero. The bound is against the OLD leading minor, and hence does not accidentally divide by a perturbed or vanishing quantity.

    theorem relative_projected_minor (p : ℕ) (b : ℕ → OrthonormalBasis ι ℝ E)
        (s : ℕ → powersetCard ι p) (A B : ℕ → E →L[ℝ] E)
        (v : ℕ → Fin p → E) (r L : ℕ → ℝ) (W : ℝ) (hW : 0 ≤ W)
        (hw : ∀ᶠ k in atTop, ‖exteriorPower.ιMulti ℝ p (v k)‖ ≤ W)
        (hL : ∀ᶠ k in atTop, |r k| ≤ |L k|)
        (he : (fun k => exterior p (B k)-exterior p (A k)) =o[atTop] r) :
        (fun k => projectedMinor (b k) p (s k) (B k) (v k)-
          projectedMinor (b k) p (s k) (A k) (v k)) =o[atTop] L := by
    …

    Mentions: OAI.SmoothObstruction.ExteriorStability.exterior, OAI.SmoothObstruction.ExteriorStability.projectedMinor

19. lemma OAI.SmoothObstruction.ExteriorStability.relative_minor_ratios line 601

    Source documentation

    Relative errors preserve nonzero leading minors and all other ratios. There is no lower absolute bound on a.

    lemma relative_minor_ratios {a a' c c' ε δ : ℝ} (ha : a ≠ 0)
        (hε : 0 ≤ ε) (hε1 : ε < 1) (hδ : 0 ≤ δ)
        (haa : |a'-a| ≤ ε*|a|) (hc : |c| ≤ δ*|a|)
        (hcc : |c'-c| ≤ ε*|a|) :
        a' ≠ 0 ∧ |c'|/|a'| ≤ (δ+ε)/(1-ε) := by
    …

20. lemma OAI.SmoothObstruction.ExteriorStability.projected_postcomposition_transfer line 633

    Source documentation

    Fixed endpoint projections preserve the all-subinterval exterior error. The multiplier is a dimension constant even for a nonpositive rate sum.

    lemma projected_postcomposition_transfer (b : OrthonormalBasis ι ℝ E)
        (p : ℕ) (r : powersetCard ι p) (Q A B : E →L[ℝ] E)
        (v : Fin p → E) (hv : ∀ i,‖v i‖≤1) {C ε : ℝ} (hC : 0≤C)
        (hQ : ‖exterior p Q‖≤C) (he : ‖exterior p B-exterior p A‖≤ε) :
        |projectedMinor b p r (Q*B) v-projectedMinor b p r (Q*A) v|≤
          C*ε*‖continuousWedge (E:=E) p‖ := by
    …

    Mentions: OAI.SmoothObstruction.ExteriorStability.exterior, OAI.SmoothObstruction.ExteriorStability.projectedMinor, OAI.SmoothObstruction.ExteriorStability.continuousWedge

21. theorem OAI.SmoothObstruction.EuclideanSplitting.common_minor_perturbation line 660

    Source documentation

    Finite, quantitative relative-minor control for a perturbed derivative in common starting/endpoint frames. Old minor bounds are DERIVED from actual finite gauges and close subspaces. The exterior perturbation is measured at the true sum-rate scale, not at an absolute determinant floor.

    theorem common_minor_perturbation
        (U V : ℕ → Matrix (Fin d) (Fin d) ℝ) (lam : Fin d → ℝ)
        (hUV : ∀ t,U t*V t=1) (hVU : ∀ t,V t*U t=1)
        (S : Finset (Fin d)) {s t : ℕ} (hst : s≤t) {γ g K C δ : ℝ}
        (hg : 0≤g) (hK : 0≤K) (hC : 0≤C) (hδ : 0≤δ)
        (hfast : ∀ j∈S,γ+g≤lam j) (hslow : ∀ j∉S,lam j≤γ-g)
        (hUs : ‖U s‖≤Real.exp K) (hUt : ‖U t‖≤Real.exp K)
        (hVs : ‖V s‖≤Real.exp K) (hVt : ‖V t‖≤Real.exp K)
        (hpoly : ∀ A : EuclideanSpace ℝ (Fin d) →L[ℝ] EuclideanSpace ℝ (Fin d),
          ‖exterior S.card A‖≤C*(max 1 ‖A‖)^S.card)
        (W G : Submodule ℝ (EuclideanSpace ℝ (Fin d)))
        (hdim : Module.finrank ℝ W=S.card)
    …

22. def OAI.SmoothObstruction.ExteriorStability.endpointMatrix line 748

    Source documentation

    Actual endpoint-coordinate matrix; columns are the represented starting vectors. Unlike the exterior-coordinate scalar formula, this uses the usual matrix convention (output row, input column).

    noncomputable def endpointMatrix (b : OrthonormalBasis ι ℝ E) (p : ℕ)
        (r : powersetCard ι p) (A : E →L[ℝ] E) {n : ℕ} (v : Fin n → E) :
        Matrix (Fin p) (Fin n) ℝ :=
    …

23. lemma OAI.SmoothObstruction.ExteriorStability.endpointMatrix_det line 753
24. lemma OAI.SmoothObstruction.ExteriorStability.endpointMatrix_update line 760
25. lemma OAI.SmoothObstruction.ExteriorStability.endpointMatrix_cramer line 775

    Source documentation

    The Cramer minor is the genuine maximal minor with one common starting fast column replaced by a common slow column. There is no symbolic-minor proxy in the comparison.

    lemma endpointMatrix_cramer (b : OrthonormalBasis ι ℝ E) (p : ℕ)
        (r : powersetCard ι p) (A : E →L[ℝ] E) (v : Fin p → E)
        {n : ℕ} (w : Fin n → E) (i : Fin p) (j : Fin n) :
        ((endpointMatrix b p r A v).updateCol i (fun k => endpointMatrix b p r A w k j)).det=
          projectedMinor b p r A (Function.update v i (w j)) := by
    …

    Mentions: OAI.SmoothObstruction.ExteriorStability.endpointMatrix, OAI.SmoothObstruction.ExteriorStability.projectedMinor

26. lemma OAI.SmoothObstruction.MinorGraph.cramer_ratio line 792
27. lemma OAI.SmoothObstruction.MinorGraph.graph_bound line 801
28. lemma OAI.SmoothObstruction.MinorGraph.block_factorization line 810
29. theorem OAI.SmoothObstruction.MinorGraph.normalized_close line 824

    Source documentation

    The modulus depends only on the two dimensions, never on the size or sign of the leading determinants.

    theorem normalized_close (ε : ℝ) (hε : 0<ε) :
        ∃ δ : ℝ,0<δ ∧ ∀ (B : Matrix m n ℝ) (C : Matrix n m ℝ),
          ‖B‖≤δ → ‖C‖≤δ → |(fromBlocks 1 B C 1).det-1|<ε := by
    …

30. theorem OAI.SmoothObstruction.MinorGraph.relative_joint_determinant line 846

    Source documentation

    Relative determinant estimate from the genuine maximal minors. In particular there is no lower bound on the leading volumes A.det and D.det.

    theorem relative_joint_determinant (ε : ℝ) (hε : 0<ε) :
        ∃ δ : ℝ,0<δ ∧ ∀ (A : Matrix m m ℝ) (B : Matrix m n ℝ)
          (C : Matrix n m ℝ) (D : Matrix n n ℝ),
          A.det≠0 → D.det≠0 →
          (∀ i j,|(A.updateCol i (fun r => B r j)).det|≤δ*|A.det|) →
          (∀ i j,|(D.updateCol i (fun r => C r j)).det|≤δ*|D.det|) →
          |(fromBlocks A B C D).det/(A.det*D.det)-1|<ε := by
    …

31. theorem OAI.SmoothObstruction.EuclideanSplitting.common_endpoint_graph_bound line 869

    Source documentation

    The genuine endpoint derivative graph in the common product basis. Cramer ratios are obtained from actual projected fast/mixed minors, not postulated as a graph-smallness assumption. Either column group may be empty.

    theorem common_endpoint_graph_bound
        (U V : ℕ → Matrix (Fin d) (Fin d) ℝ) (lam : Fin d → ℝ)
        (hUV : ∀ t,U t*V t=1) (hVU : ∀ t,V t*U t=1)
        (S : Finset (Fin d)) {s t : ℕ} (hst : s≤t) {γ g K C δ : ℝ}
        (hg : 0≤g) (hK : 0≤K) (hC : 0≤C) (hδ : 0≤δ)
        (hfast : ∀ j∈S,γ+g≤lam j) (hslow : ∀ j∉S,lam j≤γ-g)
        (hUs : ‖U s‖≤Real.exp K) (hUt : ‖U t‖≤Real.exp K)
        (hVs : ‖V s‖≤Real.exp K) (hVt : ‖V t‖≤Real.exp K)
        (hpoly : ∀ A : EuclideanSpace ℝ (Fin d) →L[ℝ] EuclideanSpace ℝ (Fin d),
          ‖exterior S.card A‖≤C*(max 1 ‖A‖)^S.card)
        (W G : Submodule ℝ (EuclideanSpace ℝ (Fin d)))
        (hdim : Module.finrank ℝ W=S.card)
    …

32. theorem OAI.SmoothObstruction.EuclideanSplitting.common_perturbed_endpoint_graph_bound line 952

    Source documentation

    The genuine endpoint derivative graph in the common product basis. The actual exterior perturbation, relative even on contracting determinant lines, is transferred to Cramer ratios without postulating graph smallness. Either column group may be empty.

    theorem common_perturbed_endpoint_graph_bound
        (U V : ℕ → Matrix (Fin d) (Fin d) ℝ) (lam : Fin d → ℝ)
        (hUV : ∀ t,U t*V t=1) (hVU : ∀ t,V t*U t=1)
        (S : Finset (Fin d)) {s t : ℕ} (hst : s≤t) {γ g K C δ : ℝ}
        (hg : 0≤g) (hK : 0≤K) (hC : 0≤C) (hδ : 0≤δ)
        (hfast : ∀ j∈S,γ+g≤lam j) (hslow : ∀ j∉S,lam j≤γ-g)
        (hUs : ‖U s‖≤Real.exp K) (hUt : ‖U t‖≤Real.exp K)
        (hVs : ‖V s‖≤Real.exp K) (hVt : ‖V t‖≤Real.exp K)
        (hpoly : ∀ A : EuclideanSpace ℝ (Fin d) →L[ℝ] EuclideanSpace ℝ (Fin d),
          ‖exterior S.card A‖≤C*(max 1 ‖A‖)^S.card)
        (W G : Submodule ℝ (EuclideanSpace ℝ (Fin d)))
        (hdim : Module.finrank ℝ W=S.card)
    …

33. theorem OAI.SmoothObstruction.EuclideanSplitting.common_leading_relative_transfer line 1068

    Source documentation

    Signed old-to-new leading-minor transfer. In combination with the proved common perturbed graph bound, this supplies the actual factors used in MinorGraph.joint_relative_transfer. It does not posit their relative error.

    theorem common_leading_relative_transfer
        (U V : ℕ → Matrix (Fin d) (Fin d) ℝ) (lam : Fin d → ℝ)
        (hUV : ∀ t,U t*V t=1) (hVU : ∀ t,V t*U t=1)
        (S : Finset (Fin d)) {s t : ℕ} (hst : s≤t) {γ g K C δ : ℝ}
        (hg : 0≤g) (hK : 0≤K) (hC : 0≤C) (hδ : 0≤δ)
        (hfast : ∀ j∈S,γ+g≤lam j) (hslow : ∀ j∉S,lam j≤γ-g)
        (hUs : ‖U s‖≤Real.exp K) (hUt : ‖U t‖≤Real.exp K)
        (hVs : ‖V s‖≤Real.exp K) (hVt : ‖V t‖≤Real.exp K)
        (hpoly : ∀ A : EuclideanSpace ℝ (Fin d) →L[ℝ] EuclideanSpace ℝ (Fin d),
          ‖exterior S.card A‖≤C*(max 1 ‖A‖)^S.card)
        (W G : Submodule ℝ (EuclideanSpace ℝ (Fin d)))
        (hdim : Module.finrank ℝ W=S.card)
    …

34. lemma OAI.SmoothObstruction.MinorGraph.triple_relative_error line 1148

    Source documentation

    Three signed relative errors compose without an absolute determinant floor. The constants here leave room for the source's four-Jacobian bound.

    lemma triple_relative_error {a b c ε : ℝ} (hε : 0≤ε) (hε1 : ε≤1)
        (ha : |a-1|≤ε) (hb : |b-1|≤ε) (hc : |c-1|≤ε) :
        |a*b*c-1|≤7*ε := by
    …

35. theorem OAI.SmoothObstruction.MinorGraph.joint_relative_transfer line 1174

    Source documentation

    The actual joint endpoint determinant, measured relative to the OLD leading volumes. Off-diagonal hypotheses are actual inverse-block entries, so common_perturbed_endpoint_graph_bound supplies precisely these bounds. Both blocks may be empty and the old leading volumes may be arbitrarily small or have either sign.

    theorem joint_relative_transfer : ∃ δ : ℝ,0<δ ∧
        ∀ (A₀ : Matrix m m ℝ) (D₀ : Matrix n n ℝ)
          (A : Matrix m m ℝ) (B : Matrix m n ℝ)
          (C : Matrix n m ℝ) (D : Matrix n n ℝ),
          A₀.det≠0 → D₀.det≠0 →
          |A.det/A₀.det-1|≤(1/100:ℝ) → |D.det/D₀.det-1|≤(1/100:ℝ) →
          (∀ i j,|(A⁻¹*B) i j|≤δ) → (∀ i j,|(D⁻¹*C) i j|≤δ) →
          |(fromBlocks A B C D).det/(A₀.det*D₀.det)-1|≤(1/10:ℝ) := by
    …