OAI/Computability/MaxCut/Games/Derivatives.lean

GitHub source file

63 declarations, 0 contain sorry, 0 declared as axioms

Actual Hybrid derivative energy in product coordinates

Parseval and affine restriction merge the selected Fourier coefficients over each actual compressed frequency. For a product splitting, explicit linear equivalences identify the quotient by the first factor with the second factor, and the first-factor subspace with its original space. Reindexing the frequency sum therefore introduces no multiplicity or normalization factor.

  1. def OAI.MaxCutGames.Appendix.Derivatives.spectralProjector line 19

    Source documentation

    Actual normalized Fourier projector onto the indices satisfying P.

    def spectralProjector (P : (F →ₗ[F2] E) → Prop) (f : (E →ₗ[F2] F) → ℝ) :
    (E →ₗ[F2] F) → ℝ :=
…
  2. theorem OAI.MaxCutGames.Appendix.Derivatives.linearCoeff_spectralProjector line 23
  3. theorem OAI.MaxCutGames.Appendix.Derivatives.spectralProjector_energy line 32
  4. theorem OAI.MaxCutGames.Appendix.Derivatives.spectralProjector_energy_le line 42
  5. theorem OAI.MaxCutGames.Appendix.Derivatives.function_eq_of_linearCoeff_eq line 50
  6. theorem OAI.MaxCutGames.Appendix.Derivatives.spectralProjector_comp line 58
  7. def OAI.MaxCutGames.Appendix.Derivatives.hybridProjector line 68
  8. def OAI.MaxCutGames.Appendix.Derivatives.hybridDerivative line 72
  9. def OAI.MaxCutGames.Appendix.Derivatives.rankProjector line 77
  10. def OAI.MaxCutGames.Appendix.Derivatives.mapDerivative line 81
  11. theorem OAI.MaxCutGames.Appendix.Derivatives.rankProjector_energy line 85
  12. def OAI.MaxCutGames.Appendix.Derivatives.selectorMultiplicity line 92
  13. theorem OAI.MaxCutGames.Appendix.Derivatives.selector_energy_sum line 96
  14. theorem OAI.MaxCutGames.Appendix.Derivatives.selector_energy_sum_le line 110
  15. theorem OAI.MaxCutGames.Appendix.Derivatives.linearCoeff_mapDerivative line 125
  16. theorem OAI.MaxCutGames.Appendix.Derivatives.mapDerivative_energy_eq_coefficients line 143
  17. theorem OAI.MaxCutGames.Appendix.Derivatives.mapDerivative_energy_le line 154

    Source documentation

    A.10 on actual normalized derivative norms.

    theorem mapDerivative_energy_le (X : F →ₗ[F2] E)
    [Fintype (X.ker →ₗ[F2] (E ⧸ X.range))]
    (f : (E →ₗ[F2] F) → ℝ) (d : ℕ)
    (hdegree : ∀ Y : F →ₗ[F2] E,
      d < Module.finrank F2 Y.range → linearCoeff f Y = 0) :
    (𝔼 N, mapDerivative X f N ^ 2) ≤
      (2 : ℝ) ^ (2 * Module.finrank F2 X.range * (d - Module.finrank F2 X.range)) *
        (𝔼 M, rankProjector X f M ^ 2) := by
…

    Mentions: OAI.MaxCutGames.Appendix.Derivatives.mapDerivative, OAI.MaxCutGames.Appendix.Derivatives.rankProjector

  18. theorem OAI.MaxCutGames.Appendix.Derivatives.mapDerivative_energy_eq_weighted_energy line 170

    Source documentation

    The coefficient-energy definition from the weighted estimate is exactly the normalized squared norm of the actual map derivative.

    theorem mapDerivative_energy_eq_weighted_energy (X : F →ₗ[F2] E)
    (f : (E →ₗ[F2] F) → ℝ) :
    (𝔼 N, mapDerivative X f N ^ 2) = WeightedFourthMoment.energy (linearCoeff f) X := by
…

    Mentions: OAI.MaxCutGames.Appendix.Derivatives.mapDerivative, OAI.MaxCutGames.Appendix.WeightedFourthMoment.energy

  19. theorem OAI.MaxCutGames.Appendix.Derivatives.weighted_fourth_derivative_energy line 181

    Source documentation

    The corrected weighted fourth-moment estimate for genuine derivative norms, with the normalized primal measure and counting frequency measure.

    theorem weighted_fourth_derivative_energy (f : (E →ₗ[F2] F) → ℝ) (d : ℕ)
    (hdegree : ∀ Y : F →ₗ[F2] E,
      d < Module.finrank F2 Y.range → linearCoeff f Y = 0) :
    (∑ X : F →ₗ[F2] E, ((2 : ℝ)⁻¹) ^ (8 * d * Module.finrank F2 X.range) *
      (𝔼 N, mapDerivative X f N ^ 2) ^ 2) ≤ 2 * (𝔼 M, f M ^ 2) ^ 2 := by
…

    Mentions: OAI.MaxCutGames.Appendix.Derivatives.mapDerivative

  20. theorem OAI.MaxCutGames.Appendix.Derivatives.spectralProjector_restriction line 196
  21. theorem OAI.MaxCutGames.Appendix.Derivatives.spectralProjector_restriction_moment_average line 221
  22. theorem OAI.MaxCutGames.Appendix.Derivatives.hybridDerivative_energy_average line 236
  23. def OAI.MaxCutGames.Appendix.Derivatives.HybridIndex line 243
  24. instance OAI.MaxCutGames.Appendix.Derivatives.hybridIndexFintype line 247
  25. def OAI.MaxCutGames.Appendix.Derivatives.hybridMomentSum line 256
  26. def OAI.MaxCutGames.Appendix.Derivatives.hybridSelectorEnergy line 260
  27. theorem OAI.MaxCutGames.Appendix.Derivatives.hybridMomentSum_le_of_uniform_energy line 265
  28. theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.linearCoeff_hybridDerivative line 318

    Source documentation

    The coefficient of an actual Hybrid derivative is the translated sum over the actual Hybrid selector and quotient-compression fiber.

    theorem linearCoeff_hybridDerivative
    (A : Submodule F2 E) (B : Submodule F2 F)
    [Fintype (B →ₗ[F2] (E ⧸ A))]
    (T : E →ₗ[F2] F) (f : (E →ₗ[F2] F) → ℝ)
    (Z : B →ₗ[F2] (E ⧸ A)) :
    linearCoeff (hybridDerivative A B T f) Z =
      ∑ S : F →ₗ[F2] E,
        if LinearIdentities.Hybrid S A B ∧ Restriction.compressFrequency A B S = Z
        then linearCoeff f S * (linearTraceCharacter S T).re else 0 := by
…
  29. theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.hybridDerivative_energy_eq_coefficients line 336

    Source documentation

    Exact normalized derivative energy, with counting measure on frequencies.

    theorem hybridDerivative_energy_eq_coefficients
    (A : Submodule F2 E) (B : Submodule F2 F)
    [Fintype (B →ₗ[F2] (E ⧸ A))]
    (T : E →ₗ[F2] F) (f : (E →ₗ[F2] F) → ℝ) :
    (𝔼 N, hybridDerivative A B T f N ^ 2) =
      ∑ Z : B →ₗ[F2] (E ⧸ A),
        (∑ S : F →ₗ[F2] E,
          if LinearIdentities.Hybrid S A B ∧ Restriction.compressFrequency A B S = Z
          then linearCoeff f S * (linearTraceCharacter S T).re else 0) ^ 2 := by
…
  30. def OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.leftRangeEquiv line 357

    Source documentation

    The first factor, regarded as its actual coordinate subspace.

    def leftRangeEquiv : B ≃ₗ[R] LinearMap.range (LinearMap.inl R B C) where
…
  31. theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.leftRangeEquiv_coe line 368
  32. def OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.quotientRightMap line 372

    Source documentation

    The second projection descends through the first-factor quotient.

    def quotientRightMap :
    ((A × U) ⧸ LinearMap.range (LinearMap.inl R A U)) →ₗ[R] U :=
…
  33. theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.quotientRightMap_mkQ line 378
  34. def OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.quotientRightEquiv line 384

    Source documentation

    The quotient by the first coordinate has the second coordinate as a canonical linear presentation.

    def quotientRightEquiv :
    ((A × U) ⧸ LinearMap.range (LinearMap.inl R A U)) ≃ₗ[R] U where
…
  35. theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.quotientRightEquiv_mkQ line 403
  36. def OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.productFrequencyEquiv line 408

    Source documentation

    The exact change of frequency coordinates for a product restriction.

    def productFrequencyEquiv :
    ((LinearMap.range (LinearMap.inl R B C)) →ₗ[R]
      ((A × U) ⧸ LinearMap.range (LinearMap.inl R A U))) ≃ (B →ₗ[R] U) where
…
  37. theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.productFrequencyEquiv_compressFrequency line 436

    Source documentation

    Actual quotient compression becomes the block compression.

    @[simp] theorem productFrequencyEquiv_compressFrequency
    (S : (B × C) →ₗ[F2] (A × U)) :
    productFrequencyEquiv (Restriction.compressFrequency
      (LinearMap.range (LinearMap.inl F2 A U))
      (LinearMap.range (LinearMap.inl F2 B C)) S) =
      (LinearMap.snd F2 A U).comp (S.comp (LinearMap.inl F2 B C)) := by
…

    Mentions: OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.productFrequencyEquiv

  38. theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.compressFrequency_eq_iff_product line 448

    Source documentation

    Equality of actual compressed frequencies is exactly equality of blocks.

    theorem compressFrequency_eq_iff_product
    (S : (B × C) →ₗ[F2] (A × U))
    (Z : (LinearMap.range (LinearMap.inl F2 B C)) →ₗ[F2]
      ((A × U) ⧸ LinearMap.range (LinearMap.inl F2 A U))) :
    Restriction.compressFrequency (LinearMap.range (LinearMap.inl F2 A U))
      (LinearMap.range (LinearMap.inl F2 B C)) S = Z ↔
    (LinearMap.snd F2 A U).comp (S.comp (LinearMap.inl F2 B C)) =
      productFrequencyEquiv Z := by
…

    Mentions: OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.productFrequencyEquiv

  39. theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.hybridDerivative_product_energy_eq_coefficients line 469

    Source documentation

    The actual Hybrid derivative energy in product coordinates. The sum is over ordinary block frequencies, with no quotient or basis multiplicity.

    theorem hybridDerivative_product_energy_eq_coefficients
    (T : (A × U) →ₗ[F2] (B × C))
    (f : ((A × U) →ₗ[F2] (B × C)) → ℝ) :
    (𝔼 N, hybridDerivative (LinearMap.range (LinearMap.inl F2 A U))
      (LinearMap.range (LinearMap.inl F2 B C)) T f N ^ 2) =
      ∑ Z : B →ₗ[F2] U,
        (∑ S : (B × C) →ₗ[F2] (A × U),
          if LinearIdentities.Hybrid S (LinearMap.range (LinearMap.inl F2 A U))
              (LinearMap.range (LinearMap.inl F2 B C)) ∧
              (LinearMap.snd F2 A U).comp (S.comp (LinearMap.inl F2 B C)) = Z
          then linearCoeff f S * (linearTraceCharacter S T).re else 0) ^ 2 := by
…
  40. def OAI.MaxCutGames.Inverse.KMSAnalytic.synthesis line 511

    Source documentation

    Fourier synthesis in the actual trace-character orthonormal basis.

    def synthesis (a : (F →ₗ[F2] E) → ℝ) : (E →ₗ[F2] F) → ℝ :=
…
  41. theorem OAI.MaxCutGames.Inverse.KMSAnalytic.coeff_synthesis line 514
  42. theorem OAI.MaxCutGames.Inverse.KMSAnalytic.synthesis_coeff line 521
  43. theorem OAI.MaxCutGames.Inverse.KMSAnalytic.eq_of_coeff_eq line 526
  44. theorem OAI.MaxCutGames.Inverse.KMSAnalytic.synthesis_inner line 532

    Source documentation

    Exact inner product of arbitrary synthesized coefficient arrays.

    theorem synthesis_inner (a b : (F →ₗ[F2] E) → ℝ) :
    (𝔼 X, synthesis a X * synthesis b X) = ∑ T, a T * b T := by
…

    Mentions: OAI.MaxCutGames.Inverse.KMSAnalytic.synthesis

  45. theorem OAI.MaxCutGames.Inverse.KMSAnalytic.synthesis_energy line 538

    Source documentation

    Exact squared norm, used for every restricted KMS component.

    theorem synthesis_energy (a : (F →ₗ[F2] E) → ℝ) :
    (𝔼 X, synthesis a X ^ 2) = ∑ T, a T ^ 2 := by
…

    Mentions: OAI.MaxCutGames.Inverse.KMSAnalytic.synthesis

  46. def OAI.MaxCutGames.Inverse.KMSAnalytic.component line 544

    Source documentation

    The component formed by retaining precisely the actual frequencies in P.

    def component (P : (F →ₗ[F2] E) → Prop) (f : (E →ₗ[F2] F) → ℝ) :
    (E →ₗ[F2] F) → ℝ :=
…
  47. theorem OAI.MaxCutGames.Inverse.KMSAnalytic.coeff_component line 548
  48. theorem OAI.MaxCutGames.Inverse.KMSAnalytic.component_energy line 553
  49. theorem OAI.MaxCutGames.Inverse.KMSAnalytic.component_energy_le line 561
  50. theorem OAI.MaxCutGames.Inverse.KMSAnalytic.component_inner_self line 568
  51. theorem OAI.MaxCutGames.Inverse.KMSAnalytic.component_comp line 577
  52. theorem OAI.MaxCutGames.Inverse.KMSAnalytic.component_orthogonal line 586

    Source documentation

    Components of disjoint frequency classes are genuinely orthogonal.

    theorem component_orthogonal (P Q : (F →ₗ[F2] E) → Prop)
    (hPQ : ∀ T, ¬ (P T ∧ Q T)) (f g : (E →ₗ[F2] F) → ℝ) :
    (𝔼 X, component P f X * component Q g X) = 0 := by
…

    Mentions: OAI.MaxCutGames.Inverse.KMSAnalytic.component

  53. def OAI.MaxCutGames.Inverse.KMSAnalytic.rankComponent line 599

    Source documentation

    The rank-level component uses actual image dimension.

    def rankComponent (i : ℕ) (f : (E →ₗ[F2] F) → ℝ) : (E →ₗ[F2] F) → ℝ :=
…
  54. theorem OAI.MaxCutGames.Inverse.KMSAnalytic.rankComponent_energy line 602
  55. theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.hybrid_frequency_rank line 640

    Source documentation

    The actual selector implies the exact rank loss for the actual compressed Fourier frequency.

    theorem hybrid_frequency_rank (A : Submodule F2 E) (B : Submodule F2 F)
    (S : F →ₗ[F2] E) (hS : LinearIdentities.Hybrid S A B) :
    Module.finrank F2 (Restriction.compressFrequency A B S).range + order A B =
      Module.finrank F2 S.range := by
…
  56. theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.linearCoeff_hybridDerivative_rankComponent_eq_zero line 656

    Source documentation

    A rank-i component has no derivative coefficient away from the exact compressed rank plus the order.

    theorem linearCoeff_hybridDerivative_rankComponent_eq_zero
    (A : Submodule F2 E) (B : Submodule F2 F)
    [Fintype (B →ₗ[F2] (E ⧸ A))]
    (T : E →ₗ[F2] F) (f : (E →ₗ[F2] F) → ℝ) (i : ℕ)
    (Z : B →ₗ[F2] (E ⧸ A))
    (hZ : Module.finrank F2 Z.range + order A B ≠ i) :
    linearCoeff (hybridDerivative A B T (rankComponent i f)) Z = 0 := by
…
  57. theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.hybridDerivative_rankComponent_eq_zero_of_lt_order line 677

    Source documentation

    If the order is larger than the selected rank, the actual derivative vanishes, including all affine translates.

    theorem hybridDerivative_rankComponent_eq_zero_of_lt_order
    (A : Submodule F2 E) (B : Submodule F2 F)
    [Fintype (B →ₗ[F2] (E ⧸ A))]
    (T : E →ₗ[F2] F) (f : (E →ₗ[F2] F) → ℝ) (i : ℕ)
    (hi : i < order A B) :
    hybridDerivative A B T (rankComponent i f) = 0 := by
…
  58. theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.hybridDerivative_rankComponent_energy_eq_support line 689

    Source documentation

    Parseval restricted to the exact rank-loss equality.

    theorem hybridDerivative_rankComponent_energy_eq_support
    (A : Submodule F2 E) (B : Submodule F2 F)
    [Fintype (B →ₗ[F2] (E ⧸ A))]
    (T : E →ₗ[F2] F) (f : (E →ₗ[F2] F) → ℝ) (i : ℕ) :
    (𝔼 N, hybridDerivative A B T (rankComponent i f) N ^ 2) =
      ∑ Z : B →ₗ[F2] (E ⧸ A) with Module.finrank F2 Z.range + order A B = i,
        linearCoeff (hybridDerivative A B T (rankComponent i f)) Z ^ 2 := by
…
  59. theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.hybridDerivative_rankComponent_energy_eq_rank line 707

    Source documentation

    Exact normalized energy is supported on compressed frequencies of rank i - order A B. This also holds above the order cutoff since every coefficient then vanishes.

    theorem hybridDerivative_rankComponent_energy_eq_rank
    (A : Submodule F2 E) (B : Submodule F2 F)
    [Fintype (B →ₗ[F2] (E ⧸ A))]
    (T : E →ₗ[F2] F) (f : (E →ₗ[F2] F) → ℝ) (i : ℕ) :
    (𝔼 N, hybridDerivative A B T (rankComponent i f) N ^ 2) =
      ∑ Z : B →ₗ[F2] (E ⧸ A) with Module.finrank F2 Z.range = i - order A B,
        linearCoeff (hybridDerivative A B T (rankComponent i f)) Z ^ 2 := by
…
  60. theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.hybridDerivative_rankComponent_energy_eq_rank_fibers line 725

    Source documentation

    The rank-restricted exact energy written in the actual compressed Fourier fibers used by the analytic estimate.

    theorem hybridDerivative_rankComponent_energy_eq_rank_fibers
    (A : Submodule F2 E) (B : Submodule F2 F)
    [Fintype (B →ₗ[F2] (E ⧸ A))]
    (T : E →ₗ[F2] F) (f : (E →ₗ[F2] F) → ℝ) (i : ℕ) :
    (𝔼 N, hybridDerivative A B T (rankComponent i f) N ^ 2) =
      ∑ Z : B →ₗ[F2] (E ⧸ A) with Module.finrank F2 Z.range = i - order A B,
        (∑ S : F →ₗ[F2] E,
          if LinearIdentities.Hybrid S A B ∧ Restriction.compressFrequency A B S = Z
          then linearCoeff (rankComponent i f) S * (linearTraceCharacter S T).re
          else 0) ^ 2 := by
…
  61. theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.productFrequencyEquiv_finrank line 746

    Source documentation

    The explicit change from quotient frequencies to blocks preserves rank.

    theorem productFrequencyEquiv_finrank
    (Z : (LinearMap.range (LinearMap.inl F2 B C)) →ₗ[F2]
      ((A × U) ⧸ LinearMap.range (LinearMap.inl F2 A U))) :
    Module.finrank F2 (productFrequencyEquiv Z).range = Module.finrank F2 Z.range := by
…

    Mentions: OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.productFrequencyEquiv

  62. theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.product_restriction_order line 758

    Source documentation

    The intrinsic restriction order agrees with the two fixed block dimensions.

    theorem product_restriction_order :
    order (LinearMap.range (LinearMap.inl F2 A U))
      (LinearMap.range (LinearMap.inl F2 B C)) =
      Module.finrank F2 A + Module.finrank F2 C := by
…
  63. theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.hybridDerivative_rankComponent_product_energy_eq_rank_fibers line 771

    Source documentation

    The actual derivative energy, restricted to the exact ordinary block rank.

    theorem hybridDerivative_rankComponent_product_energy_eq_rank_fibers
    (T : (A × U) →ₗ[F2] (B × C))
    (f : ((A × U) →ₗ[F2] (B × C)) → ℝ) (i : ℕ) :
    (𝔼 N, hybridDerivative (LinearMap.range (LinearMap.inl F2 A U))
      (LinearMap.range (LinearMap.inl F2 B C)) T (rankComponent i f) N ^ 2) =
      ∑ Z : B →ₗ[F2] U with
          Module.finrank F2 Z.range = i - (Module.finrank F2 A + Module.finrank F2 C),
        (∑ S : (B × C) →ₗ[F2] (A × U),
          if LinearIdentities.Hybrid S (LinearMap.range (LinearMap.inl F2 A U))
              (LinearMap.range (LinearMap.inl F2 B C)) ∧
              (LinearMap.snd F2 A U).comp (S.comp (LinearMap.inl F2 B C)) = Z
          then linearCoeff (rankComponent i f) S * (linearTraceCharacter S T).re
…