OAI/Computability/UniqueGames/Inverse/KMSFourthMomentMixedBaseLemmas.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

With no fixed points, the mixed energy is exactly the fixed-character energy of the actual small component. This is the base interface between the two KMS inductions; no norm estimate is assumed or altered by the identification.

  1. def OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.zeroFixedEquiv line 30

    Source documentation

    The free block is the entire product when the fixed block is zero.

    def zeroFixedEquiv : I ≃ₗ[F2] (A × I) :=
…
  2. theorem OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.zeroFixedEquiv_apply line 38
  3. theorem OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.zeroFixedEquiv_symm_apply line 41
  4. theorem OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.partialRestrict_smallComponent_zeroFixed line 57

    Source documentation

    The actual partially restricted small function in zero fixed dimension.

    theorem partialRestrict_smallComponent_zeroFixed (ι : (A × I) →ₗ[F2] E)
    (f : (E →ₗ[F2] F) → ℝ) (a : A →ₗ[F2] F) :
    partialRestrict (smallComponent ι f) a =
      smallComponent (ι.comp (LinearMap.inr F2 A I)) f := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.partialRestrict

  5. theorem OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.mixedEnergy_zeroFixed line 76

    Source documentation

    Exact base normalization for the mixed estimate: the prescribed Fourier slice is the fixed-frequency energy used by Lemma 3.19.

    theorem mixedEnergy_zeroFixed (ι : (A × I) →ₗ[F2] E)
    (f : (E →ₗ[F2] F) → ℝ) (a : A →ₗ[F2] F)
    (π : I →ₗ[F2] J) (ν : F →ₗ[F2] J) :
    sliceEnergy (fun T => π.comp T = ν) (partialRestrict (smallComponent ι f) a) =
      fixedFrequencyEnergy (ι.comp (LinearMap.inr F2 A I)) f π ν := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.sliceEnergy, OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.partialRestrict

  6. theorem OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.mixed_point_sliceEnergy_le line 121

    Source documentation

    The quantitative mixed recurrence, retaining every actual shifted center. No density or Fourier estimate is assumed in this identity-based step.

    theorem mixed_point_sliceEnergy_le (ι : (A × I) →ₗ[F2] E)
    (hι : Function.Injective ι) (f : ((E × F2) →ₗ[F2] F) → ℝ)
    (hf : KMSBasisInvariant.IsBasisInvariant f) (a : A →ₗ[F2] F) (b : F)
    (P : (F →ₗ[F2] I) → Prop) :
    sliceEnergy P (partialRestrict
      (pointRestrict (smallComponent (pointLift ι) f) b) a) ≤
      2 * (sliceEnergy P (partialRestrict (smallComponent ι (pointRestrict f b)) a) +
        (Fintype.card ((A × I) →ₗ[F2] F2) : ℝ) *
          ∑ φ : (A × I) →ₗ[F2] F2, sliceEnergy P
            (partialRestrict (smallComponent (pointPad ι) f)
              (a + (φ.smulRight b).comp (LinearMap.inl F2 A I)))) := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.KMSBasisInvariant.IsBasisInvariant, OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.sliceEnergy, OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.partialRestrict

  7. theorem OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.mixed_point_sliceEnergy_le_of_bounds line 148

    Source documentation

    The induction uses one bound on the point-restricted original function, and a bound on the lower component uniform in all previous fixed points.

    theorem mixed_point_sliceEnergy_le_of_bounds (ι : (A × I) →ₗ[F2] E)
    (hι : Function.Injective ι) (f : ((E × F2) →ₗ[F2] F) → ℝ)
    (hf : KMSBasisInvariant.IsBasisInvariant f) (a : A →ₗ[F2] F) (b : F)
    (P : (F →ₗ[F2] I) → Prop) (H₀ H₁ : ℝ)
    (h₀ : sliceEnergy P
      (partialRestrict (smallComponent ι (pointRestrict f b)) a) ≤ H₀)
    (h₁ : ∀ a' : A →ₗ[F2] F,
      sliceEnergy P (partialRestrict (smallComponent (pointPad ι) f) a') ≤ H₁) :
    sliceEnergy P (partialRestrict
      (pointRestrict (smallComponent (pointLift ι) f) b) a) ≤
      2 * (H₀ + (Fintype.card ((A × I) →ₗ[F2] F2) : ℝ) ^ 2 * H₁) := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.KMSBasisInvariant.IsBasisInvariant, OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.sliceEnergy, OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.partialRestrict

  8. theorem OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.point_sliceEnergy_le line 206

    Source documentation

    Actual one-point mixed-energy recurrence; the remaining fixed-character slice P is arbitrary, and all smaller components are the genuine functions.

    theorem point_sliceEnergy_le (ι : I →ₗ[F2] E) (hι : Function.Injective ι)
    (f : ((E × F2) →ₗ[F2] F) → ℝ) (hf : KMSBasisInvariant.IsBasisInvariant f)
    (a : F) (P : (F →ₗ[F2] I) → Prop) :
    sliceEnergy P (pointRestrict (smallComponent (pointLift ι) f) a) ≤
      2 * (sliceEnergy P (smallComponent ι (pointRestrict f a)) +
        (Fintype.card (I →ₗ[F2] F2) : ℝ) ^ 2 *
          sliceEnergy P (smallComponent (pointPad ι) f)) := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.KMSBasisInvariant.IsBasisInvariant, OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.sliceEnergy

  9. def OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.pointShuffle line 251

    Source documentation

    Put the last coordinate into the fixed block through e, keeping the free block unchanged.

    def pointShuffle (e : (A0 × F2) ≃ₗ[F2] A) :
    ((A0 × I) × F2) ≃ₗ[F2] (A × I) where
…
  10. theorem OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.pointShuffle_apply line 273
  11. theorem OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.pointShuffle_symm_apply line 277
  12. theorem OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.coprod_comp_pointShuffle line 283

    Source documentation

    Actual matrix identity placing one fixed column last.

    theorem coprod_comp_pointShuffle (e : (A0 × F2) ≃ₗ[F2] A)
    (a : A →ₗ[F2] F) (X : I →ₗ[F2] F) :
    (a.coprod X).comp (pointShuffle e).toLinearMap =
      pointAppend (((a.comp e.toLinearMap).comp (LinearMap.inl F2 A0 F2)).coprod X)
        (a (e (0, 1))) := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.pointShuffle

  13. def OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.pointShuffleTransport line 302

    Source documentation

    Express a function in the shuffled coordinates.

    def pointShuffleTransport (e : (A0 × F2) ≃ₗ[F2] A)
    (f : ((A × I) →ₗ[F2] F) → ℝ) :
    (((A0 × I) × F2) →ₗ[F2] F) → ℝ :=
…
  14. theorem OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.partialRestrict_pointRestrict_pointShuffleTransport line 309

    Source documentation

    Fixing the last column and then the remaining fixed block in shuffled coordinates is the original partial restriction, with the same free map.

    theorem partialRestrict_pointRestrict_pointShuffleTransport
    (e : (A0 × F2) ≃ₗ[F2] A)
    (f : ((A × I) →ₗ[F2] F) → ℝ) (a : A →ₗ[F2] F) :
    partialRestrict
      (pointRestrict (pointShuffleTransport e f) (a (e (0, 1))))
      ((a.comp e.toLinearMap).comp (LinearMap.inl F2 A0 F2)) =
        partialRestrict f a := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.partialRestrict, OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.pointShuffleTransport

  15. theorem OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.coefficient_hyperplane_restriction line 359

    Source documentation

    Exact codomain-restriction coefficient, reindexed by the extension vector. The sum has no cardinality normalization.

    theorem coefficient_hyperplane_restriction
    (f : (E →ₗ[F2] (B × F2)) → ℝ) (z : B →ₗ[F2] E) :
    linearCoeff (fun X => f ((LinearMap.inl F2 B F2).comp X)) z =
      ∑ u : E, linearCoeff f (hyperplaneExtend z u) := by
…
  16. theorem OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.coefficient_zoomOut_recursion line 371

    Source documentation

    KMS's genuine zoom-out recurrence, in product coordinates. The denominator is the exact number of independent extension vectors. Basis invariance is used to prove their Fourier coefficients coincide.

    theorem coefficient_zoomOut_recursion
    (f : (E →ₗ[F2] (B × F2)) → ℝ)
    (hf : KMSBasisInvariant.IsBasisInvariant f) (z : B →ₗ[F2] E)
    {v : E} (hv : v ∉ z.range) :
    linearCoeff f (hyperplaneExtend z v) =
      (linearCoeff (fun X => f ((LinearMap.inl F2 B F2).comp X)) z -
        ∑ u with u ∈ z.range, linearCoeff f (hyperplaneExtend z u)) /
      ((Fintype.card E - Fintype.card z.range : ℕ) : ℝ) := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.KMSBasisInvariant.IsBasisInvariant

  17. theorem OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.coefficient_zoomOut_mul line 384

    Source documentation

    A denominator-free form convenient for squared-norm estimates.

    theorem coefficient_zoomOut_mul
    (f : (E →ₗ[F2] (B × F2)) → ℝ)
    (hf : KMSBasisInvariant.IsBasisInvariant f) (z : B →ₗ[F2] E)
    {v : E} (hv : v ∉ z.range) :
    ((Fintype.card E - Fintype.card z.range : ℕ) : ℝ) *
        linearCoeff f (hyperplaneExtend z v) =
      linearCoeff (fun X => f ((LinearMap.inl F2 B F2).comp X)) z -
        ∑ u with u ∈ z.range, linearCoeff f (hyperplaneExtend z u) := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.KMSBasisInvariant.IsBasisInvariant

  18. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.sub_sum_sq_le_card_mul line 417

    Source documentation

    Cauchy--Schwarz with the distinguished scalar included as one extra summand. This form also handles an empty dependent branch.

    theorem sub_sum_sq_le_card_mul {C : Type*} [Fintype C]
    (x : ℝ) (a : C → ℝ) :
    (x - ∑ c, a c) ^ 2 ≤
      ((Fintype.card C : ℝ) + 1) * (x ^ 2 + ∑ c, a c ^ 2) := by
…
  19. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.coefficient_zoomOut_sq_bound line 436

    Source documentation

    An actual independent extension coefficient is controlled by its homogeneous restriction coefficient and every dependent extension.

    theorem coefficient_zoomOut_sq_bound
    (f : (E →ₗ[F2] (B × F2)) → ℝ) (hf : IsBasisInvariant f)
    (z : B →ₗ[F2] E) {v : E} (hv : v ∉ z.range) :
    (((Fintype.card E - Fintype.card z.range : ℕ) : ℝ) ^ 2) *
        linearCoeff f (hyperplaneExtend z v) ^ 2 ≤
      ((Fintype.card z.range : ℝ) + 1) *
        (linearCoeff (fun X => f ((LinearMap.inl F2 B F2).comp X)) z ^ 2 +
          ∑ u : z.range, linearCoeff f (hyperplaneExtend z u.val) ^ 2) := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.hyperplaneExtend

  20. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.coefficient_lifted_zoomOut_sq_bound line 489

    Source documentation

    The exact zoom-out square bound after embedding the small frequency space; the dependent sum is indexed by that small space itself.

    theorem coefficient_lifted_zoomOut_sq_bound
    (ι : (J × F2) →ₗ[F2] E) (hι : Function.Injective ι)
    (f : (E →ₗ[F2] (B × F2)) → ℝ) (hf : IsBasisInvariant f)
    (z : B →ₗ[F2] J) (hz : Function.Surjective z) :
    (((Fintype.card E - Fintype.card J : ℕ) : ℝ) ^ 2) *
        linearCoeff f (hyperplaneExtend ((leftEmbedding ι).comp z) (ι (0, 1))) ^ 2 ≤
      ((Fintype.card J : ℝ) + 1) *
        (linearCoeff (fun X => f ((LinearMap.inl F2 B F2).comp X))
            ((leftEmbedding ι).comp z) ^ 2 +
          ∑ w : J, linearCoeff f ((leftEmbedding ι).comp (hyperplaneExtend z w)) ^ 2) := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.hyperplaneExtend, OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.leftEmbedding

  21. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.fixedCharacter_step_sum line 512

    Source documentation

    Summing the genuine pointwise recurrence bounds every dependent branch by an actual lower-rank fixed-character energy, with no missing multiplicity.

    theorem fixedCharacter_step_sum
    (ι : (J × F2) →ₗ[F2] E) (hι : Function.Injective ι)
    (f : (E →ₗ[F2] (B × F2)) → ℝ) (hf : IsBasisInvariant f)
    (π : J →ₗ[F2] K) (A : B →ₗ[F2] K) :
    (((Fintype.card E - Fintype.card J : ℕ) : ℝ) ^ 2) *
        (∑ z ∈ Finset.univ.filter (fun z : B →ₗ[F2] J =>
            π.comp z = A ∧ Function.Surjective z),
          linearCoeff f (hyperplaneExtend ((leftEmbedding ι).comp z) (ι (0, 1))) ^ 2) ≤
      ((Fintype.card J : ℝ) + 1) *
        (fixedFrequencyEnergy (leftEmbedding ι)
          (fun X : E →ₗ[F2] B => f ((LinearMap.inl F2 B F2).comp X)) π A +
        ∑ w : J, fixedFrequencyEnergy (leftEmbedding ι) f π (hyperplaneExtend A (π w))) := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.hyperplaneExtend, OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.leftEmbedding, OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.fixedFrequencyEnergy

  22. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.comp_blockFrequency_zero line 574
  23. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.fixedFrequencyEnergy_product_step line 599

    Source documentation

    A genuine one-step recurrence in the actual restricted Fourier energy. Every term on the right has one fewer small-space dimension and one fewer fixed character.

    theorem fixedFrequencyEnergy_product_step
    (ι : (J × F2) →ₗ[F2] E) (hι : Function.Injective ι)
    (f : (E →ₗ[F2] (B × F2)) → ℝ) (hf : IsBasisInvariant f)
    (π : J →ₗ[F2] K) (A : B →ₗ[F2] K) :
    (((Fintype.card E - Fintype.card J : ℕ) : ℝ) ^ 2) *
        fixedFrequencyEnergy ι f (π.prodMap (LinearMap.id : F2 →ₗ[F2] F2))
          (A.prodMap (LinearMap.id : F2 →ₗ[F2] F2)) ≤
      (Fintype.card π.ker : ℝ) * (((Fintype.card J : ℝ) + 1) *
        (fixedFrequencyEnergy (leftEmbedding ι)
          (fun X : E →ₗ[F2] B => f ((LinearMap.inl F2 B F2).comp X)) π A +
        ∑ w : J, fixedFrequencyEnergy (leftEmbedding ι) f π (hyperplaneExtend A (π w)))) := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.fixedFrequencyEnergy, OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.leftEmbedding, OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.hyperplaneExtend

  24. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.fixedFrequencyEnergy_product_bound line 667

    Source documentation

    The fixed-character recurrence preserves the explicit quadratic constant. No local-density or Fourier bound is hidden in the scalar accounting.

    theorem fixedFrequencyEnergy_product_bound
    (ι : (J × F2) →ₗ[F2] E) (hι : Function.Injective ι)
    (f : (E →ₗ[F2] (B × F2)) → ℝ) (hf : IsBasisInvariant f)
    (π : J →ₗ[F2] K) (A : B →ₗ[F2] K) (ε : ℝ) (hε : 0 ≤ ε)
    (hfirst : (2 : ℝ) ^ ((Module.finrank F2 J + Module.finrank F2 K) *
        Module.finrank F2 E) * fixedFrequencyEnergy (leftEmbedding ι)
        (fun X : E →ₗ[F2] B => f ((LinearMap.inl F2 B F2).comp X)) π A ≤
      (2 : ℝ) ^ (4 * Module.finrank F2 J * Module.finrank F2 J) * ε)
    (hlower : ∀ w : J, (2 : ℝ) ^ ((Module.finrank F2 J + Module.finrank F2 K) *
        Module.finrank F2 E) * fixedFrequencyEnergy (leftEmbedding ι) f π
        (hyperplaneExtend A (π w)) ≤
      (2 : ℝ) ^ (4 * Module.finrank F2 J * Module.finrank F2 J) * ε) :
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.fixedFrequencyEnergy, OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.leftEmbedding, OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.hyperplaneExtend