OAI/Geometry/RCD/Harmonic/AffineValuePairings.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.RegularPointCoordinates.affineValueFamily line 16

   Source documentation

   The target, constant and coordinate values in the same order as the Hilbert family.

   def affineValueFamily {X : Type*} {n : ℕ} (w : X → ℝ) (V : X → Euclidean n) :
       Option (Option (Fin n)) → X → ℝ :=
   …

   Mentions: OAI.RegularPointCoordinates.Euclidean

2. theorem OAI.RegularPointCoordinates.affineValueFamily_representatives line 22
3. theorem OAI.RegularPointCoordinates.affineValueFamily_memLp line 35
4. theorem OAI.RegularPointCoordinates.localAffineMomentFamily_pairing line 42
5. def OAI.RegularPointCoordinates.euclideanValueMoments line 60

   Source documentation

   The affine moment family is already meaningful before harmonicity of the limit is identified.

   def euclideanValueMoments {n : ℕ} {S : ℝ} (g : Euclidean n → ℝ)
       (hg : MemLp g 2 (volume.restrict (ball 0 S))) {ρ : ℝ} (hρS : ρ≤S) :
       Option (Option (Fin n)) → Lp ℝ 2 (volume.restrict (ball (0:Euclidean n) ρ)) :=
   …

   Mentions: OAI.RegularPointCoordinates.Euclidean

6. theorem OAI.RegularPointCoordinates.euclideanValueMoments_pairing line 70
7. theorem OAI.RegularPointCoordinates.EuclideanHarmonicModel.moments_pairing line 91