OAI/Computability/MaxCut/Games/OperatorNorm.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

Native derivative norm decompositions for Appendix A.4 and A.5

The finite projector partitions and exact affine restriction transport yield norm bounds for the actual derivative operators. The cardinality factors are explicit: numerical estimates on the geometric index sets are separate lemmas.

  1. theorem OAI.MaxCutGames.Appendix.OperatorNorm.energy_sum_sq_le_card_cube line 25
  2. theorem OAI.MaxCutGames.Appendix.OperatorNorm.fourth_sum_le_card_cube line 60
  3. theorem OAI.MaxCutGames.Appendix.OperatorNorm.average_fourth_sum_le_card_cube line 65
  4. theorem OAI.MaxCutGames.Appendix.OperatorNorm.compressFrequency_eq_compress line 94
  5. theorem OAI.MaxCutGames.Appendix.OperatorNorm.nested_projector_restriction_apply line 99
  6. theorem OAI.MaxCutGames.Appendix.OperatorNorm.a5_outer_energy line 119
  7. theorem OAI.MaxCutGames.Appendix.OperatorNorm.a5_summand_energy line 177
  8. theorem OAI.MaxCutGames.Appendix.OperatorNorm.a5_energySquare_le line 237
  9. theorem OAI.MaxCutGames.Appendix.OperatorNorm.map_hybrid_fourth_average line 282
  10. theorem OAI.MaxCutGames.Appendix.OperatorNorm.a4_fourth_average_le line 306
  11. theorem OAI.MaxCutGames.Appendix.NaturalTransport.rank_arrowCongr line 369
  12. theorem OAI.MaxCutGames.Appendix.NaturalTransport.rankBelow_arrowCongr line 380
  13. theorem OAI.MaxCutGames.Appendix.NaturalTransport.trace_arrowCongr line 388
  14. theorem OAI.MaxCutGames.Appendix.NaturalTransport.character_arrowCongr line 397
  15. theorem OAI.MaxCutGames.Appendix.NaturalTransport.admissible_arrowCongr line 404
  16. theorem OAI.MaxCutGames.Appendix.NaturalTransport.derivative_embedding_range line 412
  17. theorem OAI.MaxCutGames.Appendix.NaturalTransport.linearCoeff_pullback line 447
  18. theorem OAI.MaxCutGames.Appendix.NaturalTransport.rankProjector_pullback line 460
  19. theorem OAI.MaxCutGames.Appendix.NaturalTransport.mapDerivative_energy_pullback line 472
  20. def OAI.MaxCutGames.Appendix.NaturalTransport.quotientFactor line 493
  21. theorem OAI.MaxCutGames.Appendix.NaturalTransport.quotientFactor_mkQ line 501
  22. def OAI.MaxCutGames.Appendix.NaturalTransport.outputFactor line 506
  23. theorem OAI.MaxCutGames.Appendix.NaturalTransport.outputFactor_val line 511
  24. def OAI.MaxCutGames.Appendix.NaturalTransport.parameterFactor line 514
  25. def OAI.MaxCutGames.Appendix.NaturalTransport.dualFactor line 519
  26. theorem OAI.MaxCutGames.Appendix.NaturalTransport.dualFactor_rank line 527
  27. theorem OAI.MaxCutGames.Appendix.NaturalTransport.parameterFactor_embedding line 535
  28. theorem OAI.MaxCutGames.Appendix.NaturalTransport.nested_hybridDerivative_function line 545
  29. theorem OAI.MaxCutGames.Appendix.NaturalTransport.nested_mapDerivative_energy line 568
  30. theorem OAI.MaxCutGames.Appendix.NaturalTransport.nested_mapDerivative_energySquare_average line 580
  31. theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.mem_map_equiv_iff_inline_KMSAnalyticHybridEnergyTransport line 617
  32. theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.hybrid_arrowCongr line 628

    Source documentation

    The two clauses of the actual Hybrid selector are coordinate invariant.

    theorem hybrid_arrowCongr (a : E ≃ₗ[F2] E') (b : F ≃ₗ[F2] F')
    (S : F →ₗ[F2] E) (A : Submodule F2 E) (B : Submodule F2 F) :
    LinearIdentities.Hybrid (LinearEquiv.arrowCongr b a S)
      (A.map a.toLinearMap) (B.map b.toLinearMap) ↔
      LinearIdentities.Hybrid S A B := by
…
  33. theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.restriction_admissible_arrowCongr line 661

    Source documentation

    The actual vanishing and range constraints of an affine perturbation transport to the mapped subspaces.

    theorem restriction_admissible_arrowCongr
    (a : E ≃ₗ[F2] E') (b : F ≃ₗ[F2] F')
    (M : E →ₗ[F2] F) (A : Submodule F2 E) (B : Submodule F2 F) :
    (A.map a.toLinearMap ≤ (LinearEquiv.arrowCongr a b M).ker ∧
      (LinearEquiv.arrowCongr a b M).range ≤ B.map b.toLinearMap) ↔
      (A ≤ M.ker ∧ M.range ≤ B) := by
…
  34. theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.hybrid_embedding_range line 693

    Source documentation

    Transported quotient parameters give exactly the directly transported affine perturbations; no multiplicity or normalization factor occurs.

    theorem hybrid_embedding_range (a : E ≃ₗ[F2] E') (b : F ≃ₗ[F2] F')
    (A : Submodule F2 E) (B : Submodule F2 F) :
    ((LinearEquiv.arrowCongr a b).toLinearMap.comp (embedding A B)).range =
      (embedding (A.map a.toLinearMap) (B.map b.toLinearMap)).range := by
…
  35. theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.hybridProjector_pullback line 725

    Source documentation

    The actual Fourier Hybrid projector commutes with coordinate pullback.

    theorem hybridProjector_pullback (a : E ≃ₗ[F2] E') (b : F ≃ₗ[F2] F')
    (f : (E' →ₗ[F2] F') → ℝ) (A : Submodule F2 E) (B : Submodule F2 F) :
    hybridProjector A B (fun M => f (LinearEquiv.arrowCongr a b M)) =
      fun M => hybridProjector (A.map a.toLinearMap) (B.map b.toLinearMap) f
        (LinearEquiv.arrowCongr a b M) := by
…
  36. theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.rankComponent_pullback line 736

    Source documentation

    The actual pure-rank Fourier component commutes with coordinate pullback.

    theorem rankComponent_pullback (a : E ≃ₗ[F2] E') (b : F ≃ₗ[F2] F')
    (f : (E' →ₗ[F2] F') → ℝ) (i : ℕ) :
    rankComponent i (fun M => f (LinearEquiv.arrowCongr a b M)) =
      fun M => rankComponent i f (LinearEquiv.arrowCongr a b M) := by
…
  37. theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.hybridDerivative_energy_pullback line 749

    Source documentation

    Exact normalized energy transport, with the actual Hybrid selector, quotient restriction, and affine MaxCutGames.Fourier.MatrixRestrictions.translate transported together.

    theorem hybridDerivative_energy_pullback
    (a : E ≃ₗ[F2] E') (b : F ≃ₗ[F2] F')
    (f : (E' →ₗ[F2] F') → ℝ) (A : Submodule F2 E) (B : Submodule F2 F)
    (T : E →ₗ[F2] F) :
    (𝔼 N, hybridDerivative A B T
      (fun M => f (LinearEquiv.arrowCongr a b M)) N ^ 2) =
      𝔼 N, hybridDerivative (A.map a.toLinearMap) (B.map b.toLinearMap)
        (LinearEquiv.arrowCongr a b T) f N ^ 2 := by
…
  38. theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.hybridDerivative_rankComponent_energy_pullback line 767

    Source documentation

    Pure-rank derivative energy is invariant under both coordinate changes.

    theorem hybridDerivative_rankComponent_energy_pullback
    (a : E ≃ₗ[F2] E') (b : F ≃ₗ[F2] F')
    (f : (E' →ₗ[F2] F') → ℝ) (i : ℕ)
    (A : Submodule F2 E) (B : Submodule F2 F) (T : E →ₗ[F2] F) :
    (𝔼 N, hybridDerivative A B T
      (rankComponent i (fun M => f (LinearEquiv.arrowCongr a b M))) N ^ 2) =
      𝔼 N, hybridDerivative (A.map a.toLinearMap) (B.map b.toLinearMap)
        (LinearEquiv.arrowCongr a b T) (rankComponent i f) N ^ 2 := by
…