OAI/Computability/UniqueGames/Inverse/KMSAffineRestrictionPresentationLemmas.lean

GitHub source file

70 declarations, 0 contain sorry, 0 declared as axioms

An affine map family presented by a surjective input map and an injective output map is precisely the quotient-parameter family with vanishing subspace the input kernel and target subspace the output range. Both its uniform law and its dimension budget agree exactly with the intrinsic restriction data.

  1. def OAI.UniqueGamesTheorem.Inverse.KMSAffineRestrictionPresentation.parameterEquiv line 37

    Source documentation

    Change from surjective/injective presentation coordinates to the actual quotient-domain and subspace-target parameter.

    def parameterEquiv (L : E →ₗ[F2] D) (hL : Function.Surjective L)
    (J : C →ₗ[F2] F) (hJ : Function.Injective J) :
    (D →ₗ[F2] C) ≃ₗ[F2] Parameter L.ker J.range :=
…
  2. theorem OAI.UniqueGamesTheorem.Inverse.KMSAffineRestrictionPresentation.parameterEquiv_apply_mk line 43
  3. theorem OAI.UniqueGamesTheorem.Inverse.KMSAffineRestrictionPresentation.embed_parameterEquiv line 49

    Source documentation

    The embedded quotient parameter is the original two-sided composition.

    @[simp] theorem embed_parameterEquiv (L : E →ₗ[F2] D)
    (hL : Function.Surjective L) (J : C →ₗ[F2] F)
    (hJ : Function.Injective J) (X : D →ₗ[F2] C) :
    embed L.ker J.range (parameterEquiv L hL J hJ X) = J.comp (X.comp L) := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.KMSAffineRestrictionPresentation.parameterEquiv

  4. theorem OAI.UniqueGamesTheorem.Inverse.KMSAffineRestrictionPresentation.translate_parameterEquiv line 57
  5. theorem OAI.UniqueGamesTheorem.Inverse.KMSAffineRestrictionPresentation.expect_presentation line 65

    Source documentation

    Exact uniform expectation in any presentation of the actual restriction.

    theorem expect_presentation [Finite E] [Finite F] [Fintype (D →ₗ[F2] C)]
    (L : E →ₗ[F2] D) (hL : Function.Surjective L)
    (J : C →ₗ[F2] F) (hJ : Function.Injective J)
    (T : E →ₗ[F2] F) (f : (E →ₗ[F2] F) → ℝ) :
    (𝔼 X : D →ₗ[F2] C, f (T + J.comp (X.comp L))) =
      𝔼 A : Parameter L.ker J.range, restrict f L.ker J.range T A := by
…
  6. theorem OAI.UniqueGamesTheorem.Inverse.KMSAffineRestrictionPresentation.expect_presentation_sq line 76

    Source documentation

    In particular, the normalized squared restriction norms coincide.

    theorem expect_presentation_sq [Finite E] [Finite F] [Fintype (D →ₗ[F2] C)]
    (L : E →ₗ[F2] D) (hL : Function.Surjective L)
    (J : C →ₗ[F2] F) (hJ : Function.Injective J)
    (T : E →ₗ[F2] F) (f : (E →ₗ[F2] F) → ℝ) :
    (𝔼 X : D →ₗ[F2] C, f (T + J.comp (X.comp L)) ^ 2) =
      𝔼 A : Parameter L.ker J.range, (restrict f L.ker J.range T A) ^ 2 :=
…
  7. theorem OAI.UniqueGamesTheorem.Inverse.KMSAffineRestrictionPresentation.order_add_dimensions line 86

    Source documentation

    The intrinsic restriction order is exactly the dimensions lost by the surjective input and injective output presentations.

    theorem order_add_dimensions [FiniteDimensional F2 E] [FiniteDimensional F2 F]
    (L : E →ₗ[F2] D) (hL : Function.Surjective L)
    (J : C →ₗ[F2] F) (hJ : Function.Injective J) :
    order L.ker J.range + Module.finrank F2 D + Module.finrank F2 C =
      Module.finrank F2 E + Module.finrank F2 F := by
…
  8. theorem OAI.UniqueGamesTheorem.Inverse.KMSAffineRestrictionPresentation.order_le_of_dimensions line 100

    Source documentation

    The sum-of-dimensions budget used in the fourth-moment statement implies the actual quotient/subspace restriction budget, without truncated subtraction.

    theorem order_le_of_dimensions [FiniteDimensional F2 E] [FiniteDimensional F2 F]
    (L : E →ₗ[F2] D) (hL : Function.Surjective L)
    (J : C →ₗ[F2] F) (hJ : Function.Injective J) (r : ℕ)
    (h : Module.finrank F2 E + Module.finrank F2 F ≤
      Module.finrank F2 D + Module.finrank F2 C + r) :
    order L.ker J.range ≤ r := by
…
  9. abbrev OAI.UniqueGamesTheorem.Inverse.KMSAffineRestrictionSplit.localVanishing line 135

    Source documentation

    The original vanishing subspace viewed inside the chosen large summand.

    abbrev localVanishing (D U : Submodule F2 E) : Submodule F2 U :=
…
  10. def OAI.UniqueGamesTheorem.Inverse.KMSAffineRestrictionSplit.splitLeft line 139

    Source documentation

    The constrained component of an actual quotient parameter.

    def splitLeft (D U : Submodule F2 E) (W : Submodule F2 F)
    (A : Parameter D W) : Parameter (localVanishing D U) W :=
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.KMSAffineRestrictionSplit.localVanishing

  11. theorem OAI.UniqueGamesTheorem.Inverse.KMSAffineRestrictionSplit.splitLeft_apply line 148
  12. def OAI.UniqueGamesTheorem.Inverse.KMSAffineRestrictionSplit.splitRight line 154

    Source documentation

    The free component of an actual quotient parameter.

    def splitRight (D E₀ : Submodule F2 E) (W : Submodule F2 F)
    (A : Parameter D W) : E₀ →ₗ[F2] W :=
…
  13. theorem OAI.UniqueGamesTheorem.Inverse.KMSAffineRestrictionSplit.splitRight_apply line 158
  14. def OAI.UniqueGamesTheorem.Inverse.KMSAffineRestrictionSplit.joinMap line 163

    Source documentation

    Assemble the two components before quotienting by D.

    def joinMap (D U E₀ : Submodule F2 E) (W : Submodule F2 F)
    (hc : IsCompl U E₀) (B : Parameter (localVanishing D U) W)
    (C : E₀ →ₗ[F2] W) : E →ₗ[F2] W :=
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.KMSAffineRestrictionSplit.localVanishing

  15. theorem OAI.UniqueGamesTheorem.Inverse.KMSAffineRestrictionSplit.joinMap_apply_left line 169
  16. theorem OAI.UniqueGamesTheorem.Inverse.KMSAffineRestrictionSplit.joinMap_apply_right line 175
  17. theorem OAI.UniqueGamesTheorem.Inverse.KMSAffineRestrictionSplit.joinMap_vanishes line 181
  18. def OAI.UniqueGamesTheorem.Inverse.KMSAffineRestrictionSplit.join line 194

    Source documentation

    The actual quotient parameter reconstructed from both independent pieces.

    def join (D U E₀ : Submodule F2 E) (W : Submodule F2 F)
    (hDU : D ≤ U) (hc : IsCompl U E₀)
    (B : Parameter (localVanishing D U) W) (C : E₀ →ₗ[F2] W) : Parameter D W :=
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.KMSAffineRestrictionSplit.localVanishing

  19. theorem OAI.UniqueGamesTheorem.Inverse.KMSAffineRestrictionSplit.join_apply line 199
  20. theorem OAI.UniqueGamesTheorem.Inverse.KMSAffineRestrictionSplit.join_embed_apply_left line 204
  21. theorem OAI.UniqueGamesTheorem.Inverse.KMSAffineRestrictionSplit.join_embed_apply_right line 211
  22. theorem OAI.UniqueGamesTheorem.Inverse.KMSAffineRestrictionSplit.splitLeft_join line 217
  23. theorem OAI.UniqueGamesTheorem.Inverse.KMSAffineRestrictionSplit.splitRight_join line 226
  24. theorem OAI.UniqueGamesTheorem.Inverse.KMSAffineRestrictionSplit.join_split line 234
  25. def OAI.UniqueGamesTheorem.Inverse.KMSAffineRestrictionSplit.splitEquiv line 248

    Source documentation

    Linear equivalence of the full restriction domain with the constrained component and the free complementary component.

    def splitEquiv (D U E₀ : Submodule F2 E) (W : Submodule F2 F)
    (hDU : D ≤ U) (hc : IsCompl U E₀) :
    Parameter D W ≃ₗ[F2]
      (Parameter (localVanishing D U) W × (E₀ →ₗ[F2] W)) where
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.KMSAffineRestrictionSplit.localVanishing

  26. theorem OAI.UniqueGamesTheorem.Inverse.KMSAffineRestrictionSplit.splitEquiv_symm_apply line 272
  27. instance OAI.UniqueGamesTheorem.Inverse.KMSAffineRestrictionSplit.freeFintype line 277
  28. theorem OAI.UniqueGamesTheorem.Inverse.KMSAffineRestrictionSplit.expect_join line 286

    Source documentation

    Exact product uniform sampling on the original quotient-map parameters.

    theorem expect_join [Finite E] [Finite F]
    (D U E₀ : Submodule F2 E) (W : Submodule F2 F)
    (hDU : D ≤ U) (hc : IsCompl U E₀) (f : Parameter D W → ℝ) :
    (𝔼 A : Parameter D W, f A) =
      𝔼 B : Parameter (localVanishing D U) W,
        𝔼 C : E₀ →ₗ[F2] W, f (join D U E₀ W hDU hc B C) := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.KMSAffineRestrictionSplit.localVanishing, OAI.UniqueGamesTheorem.Inverse.KMSAffineRestrictionSplit.join

  29. theorem OAI.UniqueGamesTheorem.Inverse.KMSAffineRestrictionSplit.expect_restrict line 301

    Source documentation

    The same exact split for the observable on the actual affine restriction.

    theorem expect_restrict [Finite E] [Finite F]
    (D U E₀ : Submodule F2 E) (W : Submodule F2 F)
    (hDU : D ≤ U) (hc : IsCompl U E₀) (T : E →ₗ[F2] F)
    (f : (E →ₗ[F2] F) → ℝ) :
    (𝔼 A : Parameter D W, restrict f D W T A) =
      𝔼 B : Parameter (localVanishing D U) W,
        𝔼 C : E₀ →ₗ[F2] W, f (translate D W T (join D U E₀ W hDU hc B C)) :=
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.KMSAffineRestrictionSplit.localVanishing, OAI.UniqueGamesTheorem.Inverse.KMSAffineRestrictionSplit.join

  30. def OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.synthesis line 339

    Source documentation

    Fourier synthesis in the actual trace-character orthonormal basis.

    def synthesis (a : (F →ₗ[F2] E) → ℝ) : (E →ₗ[F2] F) → ℝ :=
…
  31. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.coeff_synthesis line 342
  32. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.synthesis_coeff line 349
  33. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.eq_of_coeff_eq line 354
  34. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.synthesis_inner line 360

    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.UniqueGamesTheorem.Inverse.KMSAnalytic.synthesis

  35. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.synthesis_energy line 366

    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.UniqueGamesTheorem.Inverse.KMSAnalytic.synthesis

  36. def OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.component line 372

    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) → ℝ :=
…
  37. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.coeff_component line 376
  38. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.component_energy line 381
  39. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.component_energy_le line 389
  40. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.component_inner_self line 396
  41. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.component_comp line 405
  42. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.component_orthogonal line 414

    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.UniqueGamesTheorem.Inverse.KMSAnalytic.component

  43. def OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.rankComponent line 427

    Source documentation

    The rank-level component uses actual image dimension.

    def rankComponent (i : ℕ) (f : (E →ₗ[F2] F) → ℝ) : (E →ₗ[F2] F) → ℝ :=
…
  44. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.rankComponent_energy line 430
  45. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.sum_comp_eq_fiber_card line 467

    Source documentation

    Exact sum of a function constant on the fibers of a finite map.

    theorem sum_comp_eq_fiber_card (p : A → J) (b : J → ℝ) :
    (∑ x, b (p x)) =
      ∑ j, ((Finset.univ.filter fun x => p x = j).card : ℝ) * b j := by
…
  46. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.sum_sq_eq_fiber_card line 482
  47. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.sum_sq_eq_uniform_fiber_card line 489

    Source documentation

    If every orbit has the same size, its multiplicity factors out exactly.

    theorem sum_sq_eq_uniform_fiber_card (p : A → J) (a : A → ℝ) (b : J → ℝ)
    (hab : ∀ x, a x = b (p x)) (n : ℕ)
    (hn : ∀ j, (Finset.univ.filter fun x => p x = j).card = n) :
    (∑ x, a x ^ 2) = (n : ℝ) * ∑ j, b j ^ 2 := by
…
  48. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.fiber_constant_energy_cross_mul line 501

    Source documentation

    Two coefficient arrays with the same orbit values have exactly the ratio of their orbit multiplicities. Cross multiplication includes zero-energy functions without dividing by their norm.

    theorem fiber_constant_energy_cross_mul (p : A → J) (q : B → J)
    (hp : Function.Surjective p) (hq : Function.Surjective q)
    (a : A → ℝ) (b : B → ℝ)
    (hab : ∀ x y, p x = q y → a x = b y)
    (nA nB : ℕ)
    (hA : ∀ j, (Finset.univ.filter fun x => p x = j).card = nA)
    (hB : ∀ j, (Finset.univ.filter fun y => q y = j).card = nB) :
    (nB : ℝ) * (∑ x, a x ^ 2) = (nA : ℝ) * ∑ y, b y ^ 2 := by
…
  49. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.synthesis_energy_grouped line 535

    Source documentation

    Parseval grouped by any genuine finite classification of frequencies.

    theorem synthesis_energy_grouped (p : (F →ₗ[F2] E) → J)
    (a : (F →ₗ[F2] E) → ℝ) (b : J → ℝ) (hab : ∀ S, a S = b (p S)) :
    (𝔼 X, synthesis a X ^ 2) =
      ∑ j, ((Finset.univ.filter fun S => p S = j).card : ℝ) * b j ^ 2 := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.synthesis

  50. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.synthesis_energy_by_kernel line 545

    Source documentation

    In particular, basis-invariant coefficients may be grouped by their actual kernels. The invariance premise is supplied separately by the proved change-of-basis theorem, not by any inverse or hypercontractive hypothesis.

    theorem synthesis_energy_by_kernel [Fintype (Submodule F2 F)]
    (a : (F →ₗ[F2] E) → ℝ) (b : Submodule F2 F → ℝ)
    (hab : ∀ S, a S = b S.ker) :
    (𝔼 X, synthesis a X ^ 2) =
      ∑ K : Submodule F2 F,
        ((Finset.univ.filter fun S : F →ₗ[F2] E => S.ker = K).card : ℝ) * b K ^ 2 :=
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.synthesis

  51. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergyPhase.tracePair_prod line 583

    Source documentation

    Each frequency block pairs with the corresponding restriction of the primal map. The trace is taken on the common codomain H.

    theorem tracePair_prod (S : H →ₗ[F2] U) (T : H →ₗ[F2] V)
    (X : (U × V) →ₗ[F2] H) :
    linearTracePair X (S.prod T) =
      linearTracePair (X.comp (LinearMap.inl F2 U V)) S +
      linearTracePair (X.comp (LinearMap.inr F2 U V)) T := by
…
  52. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergyPhase.character_prod line 599

    Source documentation

    Exact complex-valued phase splitting into two frequency blocks.

    theorem character_prod (S : H →ₗ[F2] U) (T : H →ₗ[F2] V)
    (X : (U × V) →ₗ[F2] H) :
    linearTraceCharacter (S.prod T) X =
      linearTraceCharacter S (X.comp (LinearMap.inl F2 U V)) *
      linearTraceCharacter T (X.comp (LinearMap.inr F2 U V)) := by
…
  53. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergyPhase.character_prod_re line 607

    Source documentation

    The real phases multiply because every binary trace character is real.

    theorem character_prod_re (S : H →ₗ[F2] U) (T : H →ₗ[F2] V)
    (X : (U × V) →ₗ[F2] H) :
    (linearTraceCharacter (S.prod T) X).re =
      (linearTraceCharacter S (X.comp (LinearMap.inl F2 U V))).re *
      (linearTraceCharacter T (X.comp (LinearMap.inr F2 U V))).re := by
…
  54. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergyPhase.character_prod_coprod_re line 617

    Source documentation

    Splitting a primal map and its dual frequency introduces no cardinal factor: both traces remain on the common space H.

    theorem character_prod_coprod_re (S : H →ₗ[F2] U) (T : H →ₗ[F2] V)
    (a : U →ₗ[F2] H) (X : V →ₗ[F2] H) :
    (linearTraceCharacter (S.prod T) (a.coprod X)).re =
      (linearTraceCharacter S a).re * (linearTraceCharacter T X).re := by
…
  55. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergyPhase.character_assemble line 634

    Source documentation

    The three actual block phases of the assembled Hybrid frequency.

    theorem character_assemble {z : B →ₗ[F2] W}
    (p : Coordinates (A := A) (D := D) (C := C) z)
…
  56. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergyPhase.character_assemble_re line 646

    Source documentation

    The real phase factorization used in the coefficient fiber sum.

    theorem character_assemble_re {z : B →ₗ[F2] W}
    (p : Coordinates (A := A) (D := D) (C := C) z)
…
  57. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergyPhase.character_assemble_eq_fullCoordinates line 659

    Source documentation

    The ambient character is exactly the small character after restricting the primal map along the last-block embedding.

    theorem character_assemble_eq_fullCoordinates {z : B →ₗ[F2] W}
    (p : Coordinates (A := A) (D := D) (C := C) z)
…
  58. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergyPhase.character_assemble_eq_fullCoordinates_re line 668

    Source documentation

    Real-valued form of the exact small-character transport.

    theorem character_assemble_eq_fullCoordinates_re {z : B →ₗ[F2] W}
    (p : Coordinates (A := A) (D := D) (C := C) z)
…
  59. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.linearCoeff_hybridDerivative line 711

    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
…
  60. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.hybridDerivative_energy_eq_coefficients line 729

    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
…
  61. def OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.leftRangeEquiv line 750

    Source documentation

    The first factor, regarded as its actual coordinate subspace.

    def leftRangeEquiv : B ≃ₗ[R] LinearMap.range (LinearMap.inl R B C) where
…
  62. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.leftRangeEquiv_coe line 761
  63. def OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.quotientRightMap line 765

    Source documentation

    The second projection descends through the first-factor quotient.

    def quotientRightMap :
    ((A × U) ⧸ LinearMap.range (LinearMap.inl R A U)) →ₗ[R] U :=
…
  64. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.quotientRightMap_mkQ line 771
  65. def OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.quotientRightEquiv line 777

    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
…
  66. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.quotientRightEquiv_mkQ line 796
  67. def OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.productFrequencyEquiv line 801

    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
…
  68. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.productFrequencyEquiv_compressFrequency line 832

    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.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.productFrequencyEquiv

  69. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.compressFrequency_eq_iff_product line 845

    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.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.productFrequencyEquiv

  70. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.hybridDerivative_product_energy_eq_coefficients line 866

    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
…