OAI/Computability/MaxCut/Games/KMSFourthMomentPointShuffle.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

Move one fixed coordinate to the last position while preserving the free block. These are identities of actual linear maps and restricted functions; no Fourier support or analytic estimate is assumed.

  1. def OAI.MaxCutGames.Inverse.KMSFourthMoment.pointShuffle line 27

    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
…
  2. theorem OAI.MaxCutGames.Inverse.KMSFourthMoment.pointShuffle_apply line 49
  3. theorem OAI.MaxCutGames.Inverse.KMSFourthMoment.pointShuffle_symm_apply line 53
  4. theorem OAI.MaxCutGames.Inverse.KMSFourthMoment.coprod_comp_pointShuffle line 59

    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.MaxCutGames.Inverse.KMSFourthMoment.pointShuffle

  5. def OAI.MaxCutGames.Inverse.KMSFourthMoment.pointShuffleTransport line 78

    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) → ℝ :=
…
  6. theorem OAI.MaxCutGames.Inverse.KMSFourthMoment.partialRestrict_pointRestrict_pointShuffleTransport line 85

    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.MaxCutGames.Inverse.KMSFourthMoment.partialRestrict, OAI.MaxCutGames.Inverse.KMSFourthMoment.pointShuffleTransport

  7. def OAI.MaxCutGames.Inverse.KMSAnalytic.fixedFrequencyEnergy line 132

    Source documentation

    Squared small Fourier coefficients whose image under a prescribed linear projection is the fixed partial frequency.

    def fixedFrequencyEnergy (ι : I →ₗ[F2] E) (f : (E →ₗ[F2] F) → ℝ)
    (π : I →ₗ[F2] J) (A : F →ₗ[F2] J) : ℝ :=
…
  8. theorem OAI.MaxCutGames.Inverse.KMSAnalytic.fixedFrequencyEnergy_nonneg line 137
  9. theorem OAI.MaxCutGames.Inverse.KMSAnalytic.fixedFrequencyEnergy_eq line 144

    Source documentation

    The definition retains precisely the surjective compatible frequencies.

    theorem fixedFrequencyEnergy_eq (ι : I →ₗ[F2] E)
    (f : (E →ₗ[F2] F) → ℝ) (π : I →ₗ[F2] J) (A : F →ₗ[F2] J) :
    fixedFrequencyEnergy ι f π A =
      ∑ T ∈ Finset.univ.filter (fun T : F →ₗ[F2] I => π.comp T = A ∧ Function.Surjective T),
        linearCoeff f (ι.comp T) ^ 2 := by
…

    Mentions: OAI.MaxCutGames.Inverse.KMSAnalytic.fixedFrequencyEnergy

  10. theorem OAI.MaxCutGames.Inverse.KMSAnalytic.fixedFrequencyEnergy_eq_zero_of_not_surjective line 158

    Source documentation

    An impossible partial frequency contributes no energy.

    theorem fixedFrequencyEnergy_eq_zero_of_not_surjective
    (ι : I →ₗ[F2] E) (f : (E →ₗ[F2] F) → ℝ)
    (π : I →ₗ[F2] J) (hπ : Function.Surjective π)
    (A : F →ₗ[F2] J) (hA : ¬ Function.Surjective A) :
    fixedFrequencyEnergy ι f π A = 0 := by
…

    Mentions: OAI.MaxCutGames.Inverse.KMSAnalytic.fixedFrequencyEnergy

  11. theorem OAI.MaxCutGames.Inverse.KMSAnalytic.fixedFrequencyEnergy_le line 172

    Source documentation

    Forgetting the prescribed partial frequency gives the exact full small energy, so every individual restricted sum is bounded by it.

    theorem fixedFrequencyEnergy_le (ι : I →ₗ[F2] E)
    (f : (E →ₗ[F2] F) → ℝ) (π : I →ₗ[F2] J) (A : F →ₗ[F2] J) :
    fixedFrequencyEnergy ι f π A ≤ 𝔼 X, smallComponent ι f X ^ 2 := by
…

    Mentions: OAI.MaxCutGames.Inverse.KMSAnalytic.fixedFrequencyEnergy, OAI.MaxCutGames.Inverse.KMSAnalytic.smallComponent

  12. theorem OAI.MaxCutGames.Inverse.KMSAnalytic.fixedFrequencyEnergy_zero line 182

    Source documentation

    With no fixed characters the restricted sum is exactly the small squared norm; there is no ambient-cardinality normalization in the frequency sum.

    theorem fixedFrequencyEnergy_zero (ι : I →ₗ[F2] E)
    (f : (E →ₗ[F2] F) → ℝ) :
    fixedFrequencyEnergy ι f (0 : I →ₗ[F2] J) 0 =
      𝔼 X, smallComponent ι f X ^ 2 := by
…

    Mentions: OAI.MaxCutGames.Inverse.KMSAnalytic.fixedFrequencyEnergy, OAI.MaxCutGames.Inverse.KMSAnalytic.smallComponent

  13. theorem OAI.MaxCutGames.Inverse.KMSAnalytic.fixedFrequencyEnergy_eq_of_basisInvariant line 193

    Source documentation

    The fixed-character energy is independent of the chosen small-space embedding for the actual basis-invariant function.

    theorem fixedFrequencyEnergy_eq_of_basisInvariant (ι κ : I →ₗ[F2] E)
    (hι : Function.Injective ι) (hκ : Function.Injective κ)
    (f : (E →ₗ[F2] F) → ℝ) (hf : IsBasisInvariant f)
    (π : I →ₗ[F2] J) (A : F →ₗ[F2] J) :
    fixedFrequencyEnergy ι f π A = fixedFrequencyEnergy κ f π A := by
…

    Mentions: OAI.MaxCutGames.Inverse.KMSAnalytic.fixedFrequencyEnergy

  14. def OAI.MaxCutGames.Inverse.KMSAnalytic.smallFrequencyEquiv line 224

    Source documentation

    Reindex the actual dual frequency maps by an equivalence of their targets.

    def smallFrequencyEquiv (e : I ≃ₗ[F2] I') : (F →ₗ[F2] I) ≃ (F →ₗ[F2] I') where
…
  15. theorem OAI.MaxCutGames.Inverse.KMSAnalytic.smallFrequencyEquiv_apply line 230
  16. theorem OAI.MaxCutGames.Inverse.KMSAnalytic.surjective_smallFrequencyEquiv_iff line 233
  17. theorem OAI.MaxCutGames.Inverse.KMSAnalytic.smallFrequency_transport_comp line 247

    Source documentation

    Transporting the outer map in the opposite direction cancels the frequency-coordinate change.

    theorem smallFrequency_transport_comp (e : I ≃ₗ[F2] I') (π : I →ₗ[F2] J)
    (T : F →ₗ[F2] I) :
    (π.comp e.symm.toLinearMap).comp (e.toLinearMap.comp T) = π.comp T := by
…
  18. theorem OAI.MaxCutGames.Inverse.KMSAnalytic.smallCoeff_transport line 262

    Source documentation

    Exact coefficient transport; the embedding need not be injective and the original function need not be basis invariant.

    theorem smallCoeff_transport (e : I ≃ₗ[F2] I') (ι : I →ₗ[F2] E)
    (f : (E →ₗ[F2] F) → ℝ) (T : F →ₗ[F2] I) :
    smallCoeff (ι.comp e.symm.toLinearMap) f (e.toLinearMap.comp T) =
      smallCoeff ι f T := by
…

    Mentions: OAI.MaxCutGames.Inverse.KMSAnalytic.smallCoeff

  19. theorem OAI.MaxCutGames.Inverse.KMSAnalytic.fixedFrequencyEnergy_transport line 272

    Source documentation

    Prescribed partial-frequency energy is unchanged when its projection and embedding are both transported to the new small space.

    theorem fixedFrequencyEnergy_transport (e : I ≃ₗ[F2] I') (ι : I →ₗ[F2] E)
    (f : (E →ₗ[F2] F) → ℝ) (π : I →ₗ[F2] J) (A : F →ₗ[F2] J) :
    fixedFrequencyEnergy (ι.comp e.symm.toLinearMap) f
      (π.comp e.symm.toLinearMap) A = fixedFrequencyEnergy ι f π A := by
…

    Mentions: OAI.MaxCutGames.Inverse.KMSAnalytic.fixedFrequencyEnergy

  20. theorem OAI.MaxCutGames.Inverse.KMSAnalytic.smallComponent_transport line 290

    Source documentation

    The actual small-space functions agree under the corresponding primal coordinate pullback.

    theorem smallComponent_transport (e : I ≃ₗ[F2] I') (ι : I →ₗ[F2] E)
    (f : (E →ₗ[F2] F) → ℝ) (X : I' →ₗ[F2] F) :
    smallComponent (ι.comp e.symm.toLinearMap) f X =
      smallComponent ι f (X.comp e.toLinearMap) := by
…

    Mentions: OAI.MaxCutGames.Inverse.KMSAnalytic.smallComponent

  21. theorem OAI.MaxCutGames.Inverse.KMSAnalytic.smallComponent_precomp_equiv line 303

    Source documentation

    The same function identity with the new embedding written as ι ∘ g.

    theorem smallComponent_precomp_equiv (g : I ≃ₗ[F2] I') (ι : I' →ₗ[F2] E)
    (f : (E →ₗ[F2] F) → ℝ) (X : I →ₗ[F2] F) :
    smallComponent (ι.comp g.toLinearMap) f X =
      smallComponent ι f (X.comp g.symm.toLinearMap) := by
…

    Mentions: OAI.MaxCutGames.Inverse.KMSAnalytic.smallComponent

  22. def OAI.MaxCutGames.Inverse.KMSPointComplement.pointEquivOfIsCompl line 328

    Source documentation

    The coordinates supplied by a complement to a nonzero point.

    def pointEquivOfIsCompl (U : Submodule F2 E) (v : E) (hv : v ≠ 0)
    (hc : IsCompl U (Submodule.span F2 {v})) : (U × F2) ≃ₗ[F2] E :=
…
  23. theorem OAI.MaxCutGames.Inverse.KMSPointComplement.pointEquivOfIsCompl_apply line 334
  24. theorem OAI.MaxCutGames.Inverse.KMSPointComplement.exists_aligned_point_equiv line 340

    Source documentation

    Every injection with a distinguished last coordinate can be expressed as pointLift after a change of coordinates on its target.

    theorem exists_aligned_point_equiv (ι : (I × F2) →ₗ[F2] E)
    (hι : Function.Injective ι) :
    ∃ U : Submodule F2 E, ∃ e : (U × F2) ≃ₗ[F2] E,
      ∃ κ : I →ₗ[F2] U, Function.Injective κ ∧
        e.toLinearMap.comp (pointLift κ) = ι := by
…
  25. theorem OAI.MaxCutGames.Inverse.KMSPointComplement.exists_point_equiv line 373

    Source documentation

    A positive-dimensional binary space admits a last-point coordinate, with an actual subspace for the remaining coordinates and the exact dimension drop.

    theorem exists_point_equiv [FiniteDimensional F2 E]
    (h : 0 < Module.finrank F2 E) :
    ∃ U : Submodule F2 E, ∃ _e : (U × F2) ≃ₗ[F2] E,
      Module.finrank F2 U + 1 = Module.finrank F2 E := by
…
  26. theorem OAI.MaxCutGames.Inverse.KMSFourthMoment.exists_mixed_aligned_point line 405

    Source documentation

    The injection can be aligned with the fixed-point shuffle on its domain.

    theorem exists_mixed_aligned_point (ι : (A × I) →ₗ[F2] E)
    (hι : Function.Injective ι) (eA : (A0 × F2) ≃ₗ[F2] A) :
    ∃ U : Submodule F2 E, ∃ eE : (U × F2) ≃ₗ[F2] E,
      ∃ κ : (A0 × I) →ₗ[F2] U, Function.Injective κ ∧
        eE.toLinearMap.comp (pointLift κ) =
          ι.comp (pointShuffle eA).toLinearMap :=
…

    Mentions: OAI.MaxCutGames.Inverse.KMSFourthMoment.pointShuffle

  27. theorem OAI.MaxCutGames.Inverse.KMSFourthMoment.smallComponent_mixed_aligned line 430

    Source documentation

    Exact small function after both coordinate changes.

    theorem smallComponent_mixed_aligned (ι : (A × I) →ₗ[F2] E)
    (eA : (A0 × F2) ≃ₗ[F2] A) (eE : (E0 × F2) ≃ₗ[F2] E)
    (κ : (A0 × I) →ₗ[F2] E0)
    (halign : eE.toLinearMap.comp (pointLift κ) =
      ι.comp (pointShuffle eA).toLinearMap) (f : (E →ₗ[F2] F) → ℝ) :
    smallComponent (pointLift κ)
      (fun X : (E0 × F2) →ₗ[F2] F => f (X.comp eE.symm.toLinearMap)) =
      pointShuffleTransport eA (smallComponent ι f) := by
…

    Mentions: OAI.MaxCutGames.Inverse.KMSFourthMoment.pointShuffle, OAI.MaxCutGames.Inverse.KMSFourthMoment.pointShuffleTransport

  28. theorem OAI.MaxCutGames.Inverse.KMSFourthMoment.partialRestrict_smallComponent_mixed_aligned line 455

    Source documentation

    The original partially fixed small function is literally the function appearing on the left side of the actual one-point mixed recurrence.

    theorem partialRestrict_smallComponent_mixed_aligned (ι : (A × I) →ₗ[F2] E)
    (eA : (A0 × F2) ≃ₗ[F2] A) (eE : (E0 × F2) ≃ₗ[F2] E)
    (κ : (A0 × I) →ₗ[F2] E0)
    (halign : eE.toLinearMap.comp (pointLift κ) =
      ι.comp (pointShuffle eA).toLinearMap)
    (f : (E →ₗ[F2] F) → ℝ) (a : A →ₗ[F2] F) :
    partialRestrict (smallComponent ι f) a =
      partialRestrict (pointRestrict (smallComponent (pointLift κ)
        (fun X : (E0 × F2) →ₗ[F2] F => f (X.comp eE.symm.toLinearMap)))
        (a (eA (0, 1))))
        ((a.comp eA.toLinearMap).comp (LinearMap.inl F2 A0 F2)) := by
…

    Mentions: OAI.MaxCutGames.Inverse.KMSFourthMoment.pointShuffle, OAI.MaxCutGames.Inverse.KMSFourthMoment.partialRestrict

  29. def OAI.MaxCutGames.Inverse.KMSFourthMoment.zeroFixedEquiv line 487

    Source documentation

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

    def zeroFixedEquiv : I ≃ₗ[F2] (A × I) :=
…
  30. theorem OAI.MaxCutGames.Inverse.KMSFourthMoment.zeroFixedEquiv_apply line 495
  31. theorem OAI.MaxCutGames.Inverse.KMSFourthMoment.zeroFixedEquiv_symm_apply line 498
  32. theorem OAI.MaxCutGames.Inverse.KMSFourthMoment.partialRestrict_smallComponent_zeroFixed line 515

    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.MaxCutGames.Inverse.KMSFourthMoment.partialRestrict

  33. theorem OAI.MaxCutGames.Inverse.KMSFourthMoment.mixedEnergy_zeroFixed line 534

    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.MaxCutGames.Inverse.KMSFourthMoment.sliceEnergy, OAI.MaxCutGames.Inverse.KMSFourthMoment.partialRestrict

  34. theorem OAI.MaxCutGames.Inverse.KMSFourthMoment.mixed_point_sliceEnergy_le line 573

    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.MaxCutGames.Inverse.KMSBasisInvariant.IsBasisInvariant, OAI.MaxCutGames.Inverse.KMSFourthMoment.sliceEnergy, OAI.MaxCutGames.Inverse.KMSFourthMoment.partialRestrict

  35. theorem OAI.MaxCutGames.Inverse.KMSFourthMoment.mixed_point_sliceEnergy_le_of_bounds line 598

    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.MaxCutGames.Inverse.KMSBasisInvariant.IsBasisInvariant, OAI.MaxCutGames.Inverse.KMSFourthMoment.sliceEnergy, OAI.MaxCutGames.Inverse.KMSFourthMoment.partialRestrict

  36. def OAI.MaxCutGames.Inverse.KMSFourthMoment.mixedStepFactor line 633

    Source documentation

    A deliberately generous rank-dependent cost for one fixed point.

    def mixedStepFactor (R : ℕ) : ℝ := 2 ^ (2 * R + 2)
  37. theorem OAI.MaxCutGames.Inverse.KMSFourthMoment.mixedStepFactor_nonneg line 635
  38. theorem OAI.MaxCutGames.Inverse.KMSFourthMoment.one_le_mixedStepFactor line 639
  39. theorem OAI.MaxCutGames.Inverse.KMSFourthMoment.mixed_step_factor_bound line 644

    Source documentation

    Character dimension is at most the number of free coordinates, so the ambient-weight ratio has exponent at most twice the rank cap.

    theorem mixed_step_factor_bound (R t n : ℕ) (ht : t ≤ 2 * R) (hn : n ≤ R) :
    2 * ((2 : ℝ) ^ t + ((2 : ℝ) ^ n) ^ 2) ≤ mixedStepFactor R := by
…

    Mentions: OAI.MaxCutGames.Inverse.KMSFourthMoment.mixedStepFactor

  40. theorem OAI.MaxCutGames.Inverse.KMSFourthMoment.mixed_weighted_step line 662

    Source documentation

    The two lower estimates live in adjacent ambient dimensions. Multiplying by the new weight costs q on the point-restricted branch, and nothing on the unrestricted lower-component branch.

    theorem mixed_weighted_step {M A B q w n C : ℝ}
    (hq : 0 ≤ q) (hw : 0 ≤ w)
    (hrec : M ≤ 2 * (A + n ^ 2 * B))
    (hA : w * A ≤ C) (hB : (q * w) * B ≤ C) :
    (q * w) * M ≤ 2 * (q + n ^ 2) * C := by
…
  41. theorem OAI.MaxCutGames.Inverse.KMSFourthMoment.mixed_weighted_step_pow line 677

    Source documentation

    The complete scalar induction step with a rank-independent ambient weight and a rank-dependent but dimension-independent loss.

    theorem mixed_weighted_step_pow (R s ell t n : ℕ) (H ε M A B : ℝ)
    (hH : 0 ≤ H) (hε : 0 ≤ ε) (ht : t ≤ 2 * R) (hn : n ≤ R)
    (hrec : M ≤ 2 * (A + ((2 : ℝ) ^ n) ^ 2 * B))
    (hA : (2 : ℝ) ^ (t * ell) * A ≤ H * mixedStepFactor R ^ s * ε)
    (hB : (2 : ℝ) ^ (t * (ell + 1)) * B ≤ H * mixedStepFactor R ^ s * ε) :
    (2 : ℝ) ^ (t * (ell + 1)) * M ≤ H * mixedStepFactor R ^ (s + 1) * ε := by
…

    Mentions: OAI.MaxCutGames.Inverse.KMSFourthMoment.mixedStepFactor

  42. def OAI.MaxCutGames.Inverse.KMSAnalytic.HomogeneousRestrictionBound line 726

    Source documentation

    Every homogeneous output restriction of codimension at most r has the stated actual normalized squared norm. The dimension inequality avoids truncated subtraction in the restriction-composition step.

    def HomogeneousRestrictionBound (r : ℕ) (ε : ℝ) (f : (E →ₗ[F2] F) → ℝ) : Prop :=
…
  43. theorem OAI.MaxCutGames.Inverse.KMSAnalytic.HomogeneousRestrictionBound.codomain_pullback line 735

    Source documentation

    Restricting to codimension s leaves the remaining budget r. The proof uses only composition of actual injections and addition of dimensions.

    theorem HomogeneousRestrictionBound.codomain_pullback
    [FiniteDimensional F2 B] (r s : ℕ) (ε : ℝ)
    (f : (E →ₗ[F2] F) → ℝ)
    (hf : HomogeneousRestrictionBound (r + s) ε f)
    (J : B →ₗ[F2] F) (hJ : Function.Injective J)
    (hcodim : Module.finrank F2 F ≤ Module.finrank F2 B + s) :
    HomogeneousRestrictionBound r ε (fun X : E →ₗ[F2] B => f (J.comp X)) := by
…

    Mentions: OAI.MaxCutGames.Inverse.KMSAnalytic.HomogeneousRestrictionBound

  44. theorem OAI.MaxCutGames.Inverse.KMSAnalytic.HomogeneousRestrictionBound.energy_le line 747

    Source documentation

    The unrestricted squared norm is included by the identity presentation.

    theorem HomogeneousRestrictionBound.energy_le
    [FiniteDimensional F2 F] [Fintype (E →ₗ[F2] F)]
    (r : ℕ) (ε : ℝ) (f : (E →ₗ[F2] F) → ℝ)
    (hf : HomogeneousRestrictionBound r ε f) : (𝔼 X, f X ^ 2) ≤ ε := by
…

    Mentions: OAI.MaxCutGames.Inverse.KMSAnalytic.HomogeneousRestrictionBound

  45. theorem OAI.MaxCutGames.Inverse.KMSAnalytic.basisInvariant_codomain_pullback line 756

    Source documentation

    A homogeneous output restriction retains the original domain-basis invariance, as required at every step of the fixed-character induction.

    theorem basisInvariant_codomain_pullback (f : (E →ₗ[F2] F) → ℝ)
    (hf : IsBasisInvariant f) (J : B →ₗ[F2] F) :
    IsBasisInvariant (fun X : E →ₗ[F2] B => f (J.comp X)) := by
…