OAI/Combinatorics/SharpThreshold/RestrictionMassSubtype.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem313.config_sumCompl_eq_pasteCube line 19

   Source documentation

   The coordinate equivalence from a predicate and its complement is ordinary pasting.

   theorem config_sumCompl_eq_pasteCube
       (x : {i // P i} → Bool) (y : {i // ¬P i} → Bool) :
       Reindex.config (Equiv.sumCompl P) (Sum.elim x y) = pasteCube P x y := by
   …

   Mentions: OAI.Problem313.Reindex.config, OAI.Problem313.pasteCube

2. def OAI.Problem313.BiasedFourier.subtypeSupport line 28

   Source documentation

   The ambient support obtained by adjoining free and exterior supports.

   def subtypeSupport (A : Finset {i // P i}) (D : Finset {i // ¬P i}) : Finset ι :=
   …

3. theorem OAI.Problem313.BiasedFourier.coeff_restricted_coeff_subtype line 33

   Source documentation

   Conditional Fourier coefficients on arbitrary coordinate subtypes agree with full coefficients after Fourier transformation in the exterior coordinates.

   theorem coeff_restricted_coeff_subtype (p : ℝ) (f : (ι → Bool) → ℝ)
       (A : Finset {i // P i}) (D : Finset {i // ¬P i}) :
       coeff p (fun y => coeff p (restrictCube P f y) A) D =
         coeff p f (subtypeSupport P A D) := by
   …

   Mentions: OAI.Problem313.BiasedFourier.coeff, OAI.Problem313.restrictCube, OAI.Problem313.BiasedFourier.subtypeSupport

4. theorem OAI.Problem313.BiasedFourier.restricted_coeff_sq_average_subtype line 52

   Source documentation

   Exact squared-coefficient averaging over arbitrary exterior coordinate subtypes.

   theorem restricted_coeff_sq_average_subtype [DecidableEq ι] {p : ℝ} (hp : 0 < p) (hp1 : p < 1)
       (f : (ι → Bool) → ℝ) (A : Finset {i // P i}) :
       (∑ y : {i // ¬P i} → Bool, weight p y *
         (coeff p (restrictCube P f y) A) ^ 2) =
         ∑ D : Finset {i // ¬P i}, (coeff p f (subtypeSupport P A D)) ^ 2 := by
   …

   Mentions: OAI.Problem313.BiasedFourier.weight, OAI.Problem313.BiasedFourier.coeff, OAI.Problem313.restrictCube, OAI.Problem313.BiasedFourier.subtypeSupport

5. def OAI.Problem313.BiasedFourier.subtypeSupportEquiv line 63

   Source documentation

   Free and exterior support sets give each ambient support exactly once.

   def subtypeSupportEquiv :
       (Finset {i // P i} × Finset {i // ¬P i}) ≃ Finset ι :=
   …

6. theorem OAI.Problem313.BiasedFourier.subtypeSupportEquiv_apply line 69
7. theorem OAI.Problem313.BiasedFourier.subtype_subtypeSupport line 75
8. theorem OAI.Problem313.BiasedFourier.subtype_not_subtypeSupport line 83
9. theorem OAI.Problem313.BiasedFourier.sum_subtypeSupport line 90

   Source documentation

   Sum over each ambient support by its free and exterior pieces.

   theorem sum_subtypeSupport [DecidableEq ι] (h : Finset ι → ℝ) :
       (∑ A : Finset {i // P i}, ∑ D : Finset {i // ¬P i}, h (subtypeSupport P A D)) =
         ∑ S : Finset ι, h S := by
   …

   Mentions: OAI.Problem313.BiasedFourier.subtypeSupport

10. theorem OAI.Problem313.BiasedFourier.restriction_mass_subtype line 106

    Source documentation

    Exact restriction-mass transport for any statistic of the free support. There is deliberately no restriction on exterior Fourier degree.

    theorem restriction_mass_subtype [DecidableEq ι] {p : ℝ}
        (hp : 0 < p) (hp1 : p < 1) (f : (ι → Bool) → ℝ)
        (L : Finset {i // P i} → ℝ) :
        (∑ y : {i // ¬P i} → Bool, weight p y *
          ∑ A : Finset {i // P i}, L A * coeff p (restrictCube P f y) A ^ 2) =
          ∑ S : Finset ι, L (S.subtype P) * coeff p f S ^ 2 := by
    …

    Mentions: OAI.Problem313.BiasedFourier.weight, OAI.Problem313.BiasedFourier.coeff, OAI.Problem313.restrictCube

11. theorem OAI.Problem313.BiasedFourier.restriction_mass_subtype_filter line 133

    Source documentation

    Exact restricted Fourier mass at any selection of free-coordinate degrees.

    theorem restriction_mass_subtype_filter [DecidableEq ι] {p : ℝ}
        (hp : 0 < p) (hp1 : p < 1) (f : (ι → Bool) → ℝ)
        (Q : ℕ → Prop) [DecidablePred Q] :
        (∑ y : {i // ¬P i} → Bool, weight p y *
          ∑ A ∈ Finset.univ.filter (fun A : Finset {i // P i} => Q A.card),
            coeff p (restrictCube P f y) A ^ 2) =
          ∑ S ∈ Finset.univ.filter (fun S : Finset ι => Q (S.filter P).card),
            coeff p f S ^ 2 := by
    …

    Mentions: OAI.Problem313.BiasedFourier.weight, OAI.Problem313.BiasedFourier.coeff, OAI.Problem313.restrictCube

12. theorem OAI.Problem313.BiasedFourier.restriction_low_degree_mass_subtype line 146

    Source documentation

    The low-degree restriction identity in conditional-sum format.

    theorem restriction_low_degree_mass_subtype [DecidableEq ι] {p : ℝ}
        (hp : 0 < p) (hp1 : p < 1) (f : (ι → Bool) → ℝ) (k : ℝ) :
        (∑ S : Finset ι, if (S.filter P).Nonempty ∧ ((S.filter P).card : ℝ) ≤ k
          then coeff p f S ^ 2 else 0) =
          ∑ y : {i // ¬P i} → Bool, weight p y *
            ∑ A : Finset {i // P i}, if A.Nonempty ∧ (A.card : ℝ) ≤ k
              then coeff p (restrictCube P f y) A ^ 2 else 0 := by
    …

    Mentions: OAI.Problem313.BiasedFourier.coeff, OAI.Problem313.BiasedFourier.weight, OAI.Problem313.restrictCube