OAI/MeasureTheory/Falconer/Graphs/GraphSchur.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Falconer.finite_graph_schur line 20

   Source documentation

   Positive Schur bound for a complex amplitude on a finite graph.

   theorem finite_graph_schur {ι : Type*} (S : Finset ι)
       (G : ι → ι → Prop) (F : ι → ℂ) (D : ℝ)
       (hrow : ∀ a ∈ S, ((S.filter (G a)).card : ℝ) ≤ D)
       (hcol : ∀ b ∈ S, ((S.filter (fun a => G a b)).card : ℝ) ≤ D) :
       (∑ a ∈ S, ∑ b ∈ S, if G a b then ‖F a * star (F b)‖ else 0) ≤
         D * ∑ a ∈ S, ‖F a‖^2 := by
   …

2. theorem OAI.Falconer.retainedGrid_schur line 34

   Source documentation

   The retained grid graph satisfies Schur with the minimum of the two parallel-test bounds, times the explicit remaining-cell packing factor.

   theorem retainedGrid_schur {d L C₁ C₂ : ℕ} {s τ : ℝ} (hs : 0 < s)
       (hL : 4 * τ * s ≤ L) (A B : Finset (Fin d → ℤ))
       (w₁ w₂ : Space d) (hw₁ : ‖w₁‖ = 1) (hw₂ : ‖w₂‖ = 1)
       (h₁ : ∀ a ∈ A, (A.filter (fun z =>
         ‖perpendicularPart w₁ (scaledGridPoint s z - scaledGridPoint s a)‖ ≤ τ)).card ≤ C₁)
       (h₂ : ∀ b ∈ B, (B.filter (fun z =>
         ‖perpendicularPart w₂ (scaledGridPoint s z - scaledGridPoint s b)‖ ≤ τ)).card ≤ C₂)
       (F : ((Fin d → ℤ) × (Fin d → ℤ)) → ℂ) :
       (∑ row ∈ A ×ˢ B, ∑ col ∈ A ×ˢ B,
         if retainedGridEdge s w₁ w₂ τ row col then ‖F row * star (F col)‖ else 0) ≤
         ((2 * L + 1)^d * min C₁ C₂ : ℕ) * ∑ row ∈ A ×ˢ B, ‖F row‖^2 := by
   …

   Mentions: OAI.Falconer.Space, OAI.Falconer.perpendicularPart, OAI.Falconer.scaledGridPoint, OAI.Falconer.retainedGridEdge

3. theorem OAI.Falconer.partition_graph_schur line 55

   Source documentation

   Summing a nonnegative angular partition of unity preserves the Schur bound without a cap-count factor.

   theorem partition_graph_schur {ι κ : Type*} (S : Finset ι) (K : Finset κ)
       (G : κ → ι → ι → Prop) (F : ι → ℂ) (weight : κ → ℝ) (D : ℝ)
       (hweight : ∀ k ∈ K, 0 ≤ weight k) (hpartition : ∑ k ∈ K, weight k = 1)
       (hrow : ∀ k ∈ K, ∀ a ∈ S, ((S.filter (G k a)).card : ℝ) ≤ D)
       (hcol : ∀ k ∈ K, ∀ b ∈ S, ((S.filter (fun a => G k a b)).card : ℝ) ≤ D) :
       ‖∑ k ∈ K, weight k • (∑ a ∈ S, ∑ b ∈ S,
         if G k a b then F a * star (F b) else 0)‖ ≤ D * ∑ a ∈ S, ‖F a‖^2 := by
   …

4. theorem OAI.Falconer.integral_partition_graph_schur line 80

   Source documentation

   Integrated retained-edge estimate. The domain can include both angular variables and the radial variable with its nonnegative cutoff measure.

   theorem integral_partition_graph_schur {X ι κ : Type*} [MeasurableSpace X]
       (μ : Measure X) (S : Finset ι) (K : Finset κ)
       (G : κ → ι → ι → Prop) (F : ι → X → ℂ) (weight : κ → X → ℝ) (D : ℝ)
       (hF : ∀ a ∈ S, Integrable (fun x => ‖F a x‖^2) μ)
       (hweight : ∀ x k, k ∈ K → 0 ≤ weight k x)
       (hpartition : ∀ x, ∑ k ∈ K, weight k x = 1)
       (hrow : ∀ k ∈ K, ∀ a ∈ S, ((S.filter (G k a)).card : ℝ) ≤ D)
       (hcol : ∀ k ∈ K, ∀ b ∈ S, ((S.filter (fun a => G k a b)).card : ℝ) ≤ D) :
       ‖∫ x, ∑ k ∈ K, weight k x • (∑ a ∈ S, ∑ b ∈ S,
         if G k a b then F a x * star (F b x) else 0) ∂μ‖ ≤
         D * ∑ a ∈ S, ∫ x, ‖F a x‖^2 ∂μ := by
   …