OAI/Analysis/Matrix/Holder.lean

GitHub source file

73 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CoordinateSweeps.TraceHolder.inBox line 38
  2. def OAI.CoordinateSweeps.TraceHolder.tubeUnit line 40
  3. lemma OAI.CoordinateSweeps.TraceHolder.tubeUnitConvex line 43
  4. theorem OAI.CoordinateSweeps.TraceHolder.tube_barycenter line 111

    Source comment

    Equal-weight multivariate interpolation. At each vertex a single coordinate has real part card ι; all imaginary parts remain unrestricted.
    theorem tube_barycenter {f : (ι → ℂ) → ℂ} (hf : Differentiable ℂ f)
    {B : ℝ} (hB : ∀ z : ι → ℂ,
      inBox (Fintype.card ι) (fun i => (z i).re) → ‖f z‖ ≤ B)
    (hv : ∀ j, tubeUnit f (fun i => if i=j then Fintype.card ι else 0)) :
    tubeUnit f (fun _ => 1) := by
…

    Mentions: OAI.CoordinateSweeps.TraceHolder.inBox, OAI.CoordinateSweeps.TraceHolder.tubeUnit

  5. lemma OAI.CoordinateSweeps.TraceHolder.entry_norm_le line 143
  6. lemma OAI.CoordinateSweeps.TraceHolder.trace_norm_le line 153
  7. lemma OAI.CoordinateSweeps.TraceHolder.trace_diagonal_bound line 160
  8. lemma OAI.CoordinateSweeps.TraceHolder.list_prod_norm_le_one line 169
  9. lemma OAI.CoordinateSweeps.TraceHolder.differentiable_matrix_list_prod_entries line 179
  10. def OAI.CoordinateSweeps.TraceHolder.positivePower line 192
  11. lemma OAI.CoordinateSweeps.TraceHolder.positivePower_differentiable line 195
  12. lemma OAI.CoordinateSweeps.TraceHolder.positivePower_one line 201
  13. lemma OAI.CoordinateSweeps.TraceHolder.positivePower_norm_le line 206
  14. lemma OAI.CoordinateSweeps.TraceHolder.positivePower_norm_nat line 215
  15. lemma OAI.CoordinateSweeps.TraceHolder.norm_mul_diag_mul_le_one line 223
  16. def OAI.CoordinateSweeps.TraceHolder.traceFamily line 234

    Source comment

    Ordered analytic product; factors may be noncommuting.
    def traceFamily {m : ℕ} (U V : Fin m → Matrix n n ℂ) (dval : Fin m → n → ℝ)
    (z : Fin m → ℂ) : ℂ :=
…
  17. lemma OAI.CoordinateSweeps.TraceHolder.differentiable_framed_diag_entries line 238
  18. lemma OAI.CoordinateSweeps.TraceHolder.traceFamily_differentiable line 251
  19. lemma OAI.CoordinateSweeps.TraceHolder.traceFamily_bound line 274
  20. lemma OAI.CoordinateSweeps.TraceHolder.single_diagonal_trace_bound line 291
  21. lemma OAI.CoordinateSweeps.TraceHolder.traceFamily_vertex line 342
  22. theorem OAI.CoordinateSweeps.TraceHolder.diagonal_trace_holder line 360

    Source comment

    The complete normalized diagonal-factor trace Hölder estimate, for arbitrarily many NONCOMMUTING factors. It is the analytic heart of06 eq23.
    theorem diagonal_trace_holder {m : ℕ} (hm : 0 < m)
    (U V : Fin m → Matrix n n ℂ) (dval : Fin m → n → ℝ)
    (hU : ∀ j, ‖U j‖ ≤ 1) (hV : ∀ j, ‖V j‖ ≤ 1) (hdval : ∀ j i, 0 ≤ dval j i ∧ dval j i ≤ 1)
    (hs : ∀ j, ∑ i, (dval j i)^m ≤ 1) :
    ‖Matrix.trace ((List.ofFn (fun j => U j*Matrix.diagonal
      (fun i => ((dval j i : ℝ) : ℂ))*V j)).prod)‖ ≤ 1 := by
…
  23. abbrev OAI.CoordinateSweeps.TraceHolder.gramHermitian line 381
  24. def OAI.CoordinateSweeps.TraceHolder.singular line 383
  25. def OAI.CoordinateSweeps.TraceHolder.rightBasis line 385
  26. def OAI.CoordinateSweeps.TraceHolder.rawPolar line 388
  27. def OAI.CoordinateSweeps.TraceHolder.leftFrame line 391
  28. lemma OAI.CoordinateSweeps.TraceHolder.singular_nonneg line 394
  29. lemma OAI.CoordinateSweeps.TraceHolder.singular_sq line 396
  30. lemma OAI.CoordinateSweeps.TraceHolder.rawPolar_gram line 400
  31. lemma OAI.CoordinateSweeps.TraceHolder.zero_gram_column line 409
  32. lemma OAI.CoordinateSweeps.TraceHolder.rawPolar_zero_column line 420
  33. lemma OAI.CoordinateSweeps.TraceHolder.leftFrame_gram line 426
  34. lemma OAI.CoordinateSweeps.TraceHolder.leftFrame_norm_le line 441
  35. lemma OAI.CoordinateSweeps.TraceHolder.rightBasis_star_norm_le line 450
  36. lemma OAI.CoordinateSweeps.TraceHolder.polar_factors line 459
  37. lemma OAI.CoordinateSweeps.TraceHolder.trace_moment_singular line 474
  38. def OAI.CoordinateSweeps.TraceHolder.singularMass line 490
  39. def OAI.CoordinateSweeps.TraceHolder.schatten line 492
  40. lemma OAI.CoordinateSweeps.TraceHolder.singularMass_nonneg line 494
  41. lemma OAI.CoordinateSweeps.TraceHolder.singularMass_eq_zero line 497
  42. lemma OAI.CoordinateSweeps.TraceHolder.schatten_nonneg line 509
  43. lemma OAI.CoordinateSweeps.TraceHolder.schatten_pos line 512
  44. lemma OAI.CoordinateSweeps.TraceHolder.schatten_pow line 517
  45. lemma OAI.CoordinateSweeps.TraceHolder.normalized_singular_sum line 521
  46. lemma OAI.CoordinateSweeps.TraceHolder.normalized_singular_le line 527
  47. lemma OAI.CoordinateSweeps.TraceHolder.normalized_polar line 539
  48. lemma OAI.CoordinateSweeps.TraceHolder.list_prod_scaled line 554
  49. theorem OAI.CoordinateSweeps.TraceHolder.matrix_trace_holder line 564

    Source comment

    Genuine unnormalized Schatten trace Holder, built from the archived complete interpolation and polar-frame proofs rather than assumed.
    theorem matrix_trace_holder [Nonempty n] {m : ℕ} (hm : 0 < m) (A : Fin m → Matrix n n ℂ) :
    ‖Matrix.trace (List.ofFn A).prod‖ ≤ ∏ j, schatten m (A j) := by
…

    Mentions: OAI.CoordinateSweeps.TraceHolder.schatten

  50. lemma OAI.CoordinateSweeps.TraceHolder.schatten_even_eq line 593
  51. lemma OAI.CoordinateSweeps.TraceHolder.trace_mul_pow_comm line 604
  52. lemma OAI.CoordinateSweeps.TraceHolder.schatten_adjoint_even line 611
  53. lemma OAI.CoordinateSweeps.TraceHolder.trace_moment_norm line 616
  54. lemma OAI.CoordinateSweeps.TraceHolder.schatten_even_pow line 629
  55. lemma OAI.CoordinateSweeps.TraceHolder.schatten_zero_even line 634
  56. lemma OAI.CoordinateSweeps.TraceHolder.matrix_trace_holder_list line 640
  57. def OAI.CoordinateSweeps.TraceHolder.oddWord line 647

    Source comment

    Odd alternating word completing one Gram trace to an even moment.
    def oddWord (q : ℕ) (A : Matrix n n ℂ) : List (Matrix n n ℂ) :=
…
  58. lemma OAI.CoordinateSweeps.TraceHolder.oddWord_length line 651
  59. lemma OAI.CoordinateSweeps.TraceHolder.oddWord_prod line 656
  60. lemma OAI.CoordinateSweeps.TraceHolder.oddWord_schatten_prod line 660
  61. theorem OAI.CoordinateSweeps.TraceHolder.schatten_even_sum_le line 670

    Source comment

    The literal unnormalized even Schatten triangle inequality, for a finite sum, derived from genuine matrix trace Holder rather than postulated.
    theorem schatten_even_sum_le [Nonempty n] {I : Type*} [Fintype I] (q : ℕ) (hq : 0 < q)
    (A : I → Matrix n n ℂ) :
    schatten (2*q) (∑ i, A i) ≤ ∑ i, schatten (2*q) (A i) := by
…

    Mentions: OAI.CoordinateSweeps.TraceHolder.schatten

  62. lemma OAI.CoordinateSweeps.TraceHolder.matrix_trace_holder_contractions line 717
  63. lemma OAI.CoordinateSweeps.TraceHolder.matrix_trace_holder_mixed line 750
  64. lemma OAI.CoordinateSweeps.TraceHolder.matrix_trace_holder_mixed_list line 778
  65. theorem OAI.CoordinateSweeps.TraceHolder.schatten_even_mul_right line 792

    Source comment

    Right ideal inequality for the exact even Schatten norm.
    theorem schatten_even_mul_right (q : ℕ) (hq : 0 < q) (A C : Matrix n n ℂ) :
    schatten (2*q) (A*C) ≤ schatten (2*q) A * ‖C‖ := by
…

    Mentions: OAI.CoordinateSweeps.TraceHolder.schatten

  66. lemma OAI.CoordinateSweeps.TraceHolder.norm_le_schatten line 826
  67. lemma OAI.CoordinateSweeps.TraceHolder.schatten_even_mul_left line 844
  68. theorem OAI.CoordinateSweeps.TraceHolder.schatten_even_three line 852

    Source comment

    The exact three factor inequality used by06:eq20.
    theorem schatten_even_three (q : ℕ) (hq : 0 < q) (A B C : Matrix n n ℂ) :
    schatten (2*q) (A*B*C) ≤ schatten (2*q) A * ‖B‖ * schatten (2*q) C := by
…

    Mentions: OAI.CoordinateSweeps.TraceHolder.schatten

  69. lemma OAI.CoordinateSweeps.TraceHolder.schatten_even_smul_le line 860
  70. lemma OAI.CoordinateSweeps.TraceHolder.projector_norm_le line 870
  71. theorem OAI.CoordinateSweeps.TraceHolder.row_column_schatten line 879

    Source comment

    Exact resolution-of-two-subgroups inequality used in source06:eq20. No orthogonality or occurrence is silently supplied: identity and idempotence are explicit algebraic premises discharged by the genuine type resolution.
    theorem row_column_schatten {I J : Type*} [Fintype I] [Fintype J]
    (q : ℕ) (hq : 0 < q) (PR : I → Matrix n n ℂ) (PC : J → Matrix n n ℂ)
    (hR : ∑ i, PR i=1) (hC : ∑ j, PC j=1)
    (hR2 : ∀ i, PR i*PR i=PR i) (hC2 : ∀ j, PC j*PC j=PC j)
    (P X Y : Matrix n n ℂ) :
    schatten (2*q) (Y*P*X) ≤
      ∑ ij : J × I, schatten (2*q) (Y*PC ij.1)*
        ‖PC ij.1*P*PR ij.2‖*schatten (2*q) (PR ij.2*X) := by
…

    Mentions: OAI.CoordinateSweeps.TraceHolder.schatten

  72. lemma OAI.CoordinateSweeps.TraceHolder.contraction_power_from_overlap line 902
  73. theorem OAI.CoordinateSweeps.TraceHolder.row_column_moment line 916

    Source comment

    Algebraic cancellation of subgroup dimensions, preserving the absolute (not normalized) even moment. This is the quantitative core of06:eq21.
    theorem row_column_moment {I J : Type*} [Fintype I] [Fintype J]
    (q : ℕ) (hq : 0 < q) (PR : I → Matrix n n ℂ) (PC : J → Matrix n n ℂ)
    (hR : ∑ i, PR i=1) (hC : ∑ j, PC j=1)
    (hR2 : ∀ i, PR i*PR i=PR i) (hC2 : ∀ j, PC j*PC j=PC j)
    (P X Y : Matrix n n ℂ) (FR : I → ℝ) (FC : J → ℝ) (F A B c : ℝ)
    (hc : 0 ≤ c) (hcq : c ≤ q)
    (hchild : ∀ i j,
      (Matrix.trace (((PR i*X).conjTranspose*(PR i*X))^q)).re *
        (Matrix.trace (((Y*PC j).conjTranspose*(Y*PC j))^q)).re ≤
          Real.exp (-c*(FR i+FC j)+A))
    (hoverlap : ∀ i j, ‖PC j*P*PR i‖^2 ≤ Real.exp (FR i+FC j-F+B))
    (hcontract : ∀ i j, ‖PC j*P*PR i‖ ≤ 1) :
…

    Mentions: OAI.CoordinateSweeps.c