OAI/Topology/CoarseAssembly/AveragingEnergy.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CoarseAssembly.translationEnergy line 15
2. theorem OAI.CoarseAssembly.translationEnergy_nonneg line 20
3. theorem OAI.CoarseAssembly.translation_real_inner line 25
4. theorem OAI.CoarseAssembly.meanTranslation_real_inner line 36
5. theorem OAI.CoarseAssembly.lazyAverage_norm_sq_le line 56

   Source documentation

   Laziness turns the displacement-energy bound into a norm-square loss.

   theorem lazyAverage_norm_sq_le (S : Finset ArithmeticGroup) (hS : S.Nonempty)
       (k : ℕ) (x : lp (fun _ : Quotient k => H) 2) :
       ‖lazyAverage S k x‖ ^ 2 ≤
         ‖x‖ ^ 2 - translationEnergy S k x / (4 * S.card) := by
   …

   Mentions: OAI.CoarseAssembly.lazyAverage, OAI.CoarseAssembly.translationEnergy

6. theorem OAI.CoarseAssembly.constantProjection_complement_zero line 77
7. theorem OAI.CoarseAssembly.constantProjection_complement_norm_le line 84
8. theorem OAI.CoarseAssembly.uniformAveragingGap_of_energy line 102

   Source documentation

   A uniform energy estimate off the constants implies the precise norm contraction used by the spatial transfer.

   theorem uniformAveragingGap_of_energy (S : Finset ArithmeticGroup) (hS : S.Nonempty)
       (ε : ℝ) (hε : 0 < ε) (hεcard : ε ≤ 4 * S.card)
       (henergy : ∀ (k : ℕ) (x : lp (fun _ : Quotient k => H) 2),
         constantProjection (Quotient k) x = 0 →
           ε * ‖x‖ ^ 2 ≤ translationEnergy S k x) : UniformAveragingGap S H := by
   …

   Mentions: OAI.CoarseAssembly.constantProjection, OAI.CoarseAssembly.translationEnergy, OAI.CoarseAssembly.UniformAveragingGap