OAI/Analysis/Brenier/TriangularDomination.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem358.TriangularDomination.WeightedDomination line 14

   Source documentation

   A weighted change of variables that only needs an upper change-of-variables bound.

   def WeightedDomination {A B : Type*} [MeasurableSpace A] [MeasurableSpace B]
       (μ : Measure A) (ν : Measure B) (F : A → B) (J : A → ℝ≥0∞) : Prop :=
   …

2. theorem OAI.Problem358.TriangularDomination.weightedDomination_of_measurePreserving line 20

   Source documentation

   A measure-preserving coordinate change has unit weight.

   theorem weightedDomination_of_measurePreserving
       {A B : Type*} [MeasurableSpace A] [MeasurableSpace B]
       {μ : Measure A} {ν : Measure B} {F : A → B}
       (hF : MeasurePreserving F μ ν) :
       WeightedDomination μ ν F (fun _ => 1) := by
   …

   Mentions: OAI.Problem358.TriangularDomination.WeightedDomination

3. theorem OAI.Problem358.TriangularDomination.WeightedDomination.comp line 30

   Source documentation

   Weighted domination composes, multiplying the two Jacobian weights. This also allows measure-preserving coordinate identifications to be inserted on either side.

   theorem WeightedDomination.comp
       {A B C : Type*} [MeasurableSpace A] [MeasurableSpace B] [MeasurableSpace C]
       {μ : Measure A} {ν : Measure B} {ρ : Measure C}
       {F : A → B} {G : B → C} {J : A → ℝ≥0∞} {K : B → ℝ≥0∞}
       (hF : WeightedDomination μ ν F J) (hG : WeightedDomination ν ρ G K)
       (hGmeas : Measurable G) (hK : Measurable K) :
       WeightedDomination μ ρ (G ∘ F) (fun a => J a * K (F a)) := by
   …

   Mentions: OAI.Problem358.TriangularDomination.WeightedDomination

4. theorem OAI.Problem358.TriangularDomination.WeightedDomination.triangular_ae line 48

   Source documentation

   One genuine induction step for triangular changes of variables. The last output coordinate may depend on every preceding input coordinate, but the preceding output coordinates do not depend on the last input coordinate. No joint differentiability is needed: measurable weights and the two lower-dimensional integral bounds suffice.

   theorem WeightedDomination.triangular_ae
       {A B C D : Type*} [MeasurableSpace A] [MeasurableSpace B]
       [MeasurableSpace C] [MeasurableSpace D]
       {μ : Measure A} {ν : Measure B} {ρ : Measure C} {σ : Measure D}
       [SFinite ρ] [SFinite σ]
       {F : A → B} {G : A → C → D}
       {J : A → ℝ≥0∞} {j : A → C → ℝ≥0∞}
       (hF : Measurable F) (hG : Measurable (fun p : A × C => G p.1 p.2))
       (hJ : Measurable J) (hj : Measurable (fun p : A × C => j p.1 p.2))
       (hbase : WeightedDomination μ ν F J)
       (hfiber : ∀ᵐ a ∂μ, WeightedDomination ρ σ (G a) (j a)) :
       WeightedDomination (μ.prod ρ) (ν.prod σ)
   …

   Mentions: OAI.Problem358.TriangularDomination.WeightedDomination

5. theorem OAI.Problem358.TriangularDomination.WeightedDomination.triangular line 90

   Source documentation

   Everywhere fiber bounds specialize the almost-everywhere product theorem.

   theorem WeightedDomination.triangular
       {A B C D : Type*} [MeasurableSpace A] [MeasurableSpace B]
       [MeasurableSpace C] [MeasurableSpace D]
       {μ : Measure A} {ν : Measure B} {ρ : Measure C} {σ : Measure D}
       [SFinite ρ] [SFinite σ]
       {F : A → B} {G : A → C → D}
       {J : A → ℝ≥0∞} {j : A → C → ℝ≥0∞}
       (hF : Measurable F) (hG : Measurable (fun p : A × C => G p.1 p.2))
       (hJ : Measurable J) (hj : Measurable (fun p : A × C => j p.1 p.2))
       (hbase : WeightedDomination μ ν F J)
       (hfiber : ∀ a, WeightedDomination ρ σ (G a) (j a)) :
       WeightedDomination (μ.prod ρ) (ν.prod σ)
   …

   Mentions: OAI.Problem358.TriangularDomination.WeightedDomination

6. theorem OAI.Problem358.TriangularDomination.WeightedDomination.mono_weight line 107

   Source documentation

   A pointwise smaller weight preserves the integral domination.

   theorem WeightedDomination.mono_weight
       {A B : Type*} [MeasurableSpace A] [MeasurableSpace B]
       {μ : Measure A} {ν : Measure B} {F : A → B} {J K : A → ℝ≥0∞}
       (h : WeightedDomination μ ν F J) (hK : K ≤ᵐ[μ] J) :
       WeightedDomination μ ν F K := by
   …

   Mentions: OAI.Problem358.TriangularDomination.WeightedDomination

7. theorem OAI.Problem358.TriangularDomination.WeightedDomination.map_withDensity_le line 119

   Source documentation

   Integral domination gives the expected domination of weighted image measures.

   theorem WeightedDomination.map_withDensity_le
       {A B : Type*} [MeasurableSpace A] [MeasurableSpace B]
       {μ : Measure A} {ν : Measure B} {F : A → B} {J : A → ℝ≥0∞}
       (h : WeightedDomination μ ν F J) (hF : Measurable F) :
       Measure.map F (μ.withDensity J) ≤ ν := by
   …

   Mentions: OAI.Problem358.TriangularDomination.WeightedDomination

8. theorem OAI.Problem358.TriangularDomination.WeightedDomination.smul_map_le line 136

   Source documentation

   A uniform lower Jacobian bound gives the unweighted pushforward bound.

   theorem WeightedDomination.smul_map_le
       {A B : Type*} [MeasurableSpace A] [MeasurableSpace B]
       {μ : Measure A} {ν : Measure B} {F : A → B} {J : A → ℝ≥0∞}
       (h : WeightedDomination μ ν F J) (hF : Measurable F)
       {c : ℝ≥0∞} (hc : ∀ᵐ a ∂μ, c ≤ J a) :
       c • Measure.map F μ ≤ ν := by
   …

   Mentions: OAI.Problem358.TriangularDomination.WeightedDomination

9. theorem OAI.Problem358.TriangularDomination.sqrt_prod_mul_prod_le_prod_midpoint line 147

   Source documentation

   The product arithmetic-geometric-mean bound needed for diagonal derivatives of midpoints of triangular maps. Zero derivatives are allowed.

   theorem sqrt_prod_mul_prod_le_prod_midpoint
       {ι : Type*} (s : Finset ι) (a b : ι → ℝ)
       (ha : ∀ i ∈ s, 0 ≤ a i) (hb : ∀ i ∈ s, 0 ≤ b i) :
       Real.sqrt ((∏ i ∈ s, a i) * ∏ i ∈ s, b i) ≤
         ∏ i ∈ s, (a i + b i) / 2 := by
   …

10. def OAI.Problem358.TriangularDensity.geometricWeight line 183

    Source documentation

    Product of the geometric means of the paired longitudinal derivatives.

    def geometricWeight (q r dq dr : ConditionalFamily) :
        (n : ℕ) → Coordinates n → ℝ≥0∞
      | 0, _ => 1
      | n + 1, u => geometricWeight q r dq dr n (Fin.init u) *
          ENNReal.ofReal (Real.sqrt
            (dq n (sample q n (Fin.init u)) (u (Fin.last n)) *
             dr n (sample r n (Fin.init u)) (u (Fin.last n))))

    Mentions: OAI.Problem358.TriangularDensity.Coordinates

11. theorem OAI.Problem358.TriangularDensity.geometricWeight_zero line 191
12. theorem OAI.Problem358.TriangularDensity.geometricWeight_snoc line 194
13. theorem OAI.Problem358.TriangularDensity.measurable_geometricWeight_of_le line 202

    Source documentation

    Measurability requires no sign conditions or information above the cutoff.

    theorem measurable_geometricWeight_of_le (q r dq dr : ConditionalFamily) (N : ℕ)
        (hQ : ∀ n, n ≤ N → Measurable (sample q n))
        (hR : ∀ n, n ≤ N → Measurable (sample r n))
        (hD : ∀ n, n < N → Measurable (fun p : Coordinates n × ℝ => dq n p.1 p.2))
        (hE : ∀ n, n < N → Measurable (fun p : Coordinates n × ℝ => dr n p.1 p.2)) :
        ∀ n, n ≤ N → Measurable (geometricWeight q r dq dr n) := by
    …

    Mentions: OAI.Problem358.TriangularDensity.Coordinates, OAI.Problem358.TriangularDensity.geometricWeight

14. theorem OAI.Problem358.TriangularDensity.geometricWeight_eq_ofReal_sqrt_diagonalProduct line 228

    Source documentation

    On the open parameter cube, the geometric weight is exactly the geometric mean of both diagonal derivative products. This is deliberately not claimed outside the cube, where the supplied derivative fields need not be positive.

    theorem geometricWeight_eq_ofReal_sqrt_diagonalProduct
        (q r dq dr : ConditionalFamily) (N : ℕ)
        (hD : ∀ n, n < N → ∀ u, InUnitCube u → ∀ t ∈ Ioo (0 : ℝ) 1,
          0 < dq n (sample q n u) t)
        (hE : ∀ n, n < N → ∀ u, InUnitCube u → ∀ t ∈ Ioo (0 : ℝ) 1,
          0 < dr n (sample r n u) t) :
        ∀ n, n ≤ N → ∀ u, InUnitCube u →
          geometricWeight q r dq dr n u = ENNReal.ofReal (Real.sqrt
            (diagonalProduct q dq n u * diagonalProduct r dr n u)) := by
    …

    Mentions: OAI.Problem358.TriangularDensity.InUnitCube, OAI.Problem358.TriangularDensity.geometricWeight, OAI.Problem358.TriangularDensity.diagonalProduct

15. theorem OAI.Problem358.TriangularDensity.geometricWeight_ae_eq_constant line 264

    Source documentation

    Constant terminal products turn the Jacobian into a constant almost certainly, exactly the normalization needed by midpoint measure domination.

    theorem geometricWeight_ae_eq_constant
        (q r dq dr : ConditionalFamily) (N : ℕ) (A B : ℝ)
        (hD : ∀ n, n < N → ∀ u, InUnitCube u → ∀ t ∈ Ioo (0 : ℝ) 1,
          0 < dq n (sample q n u) t)
        (hE : ∀ n, n < N → ∀ u, InUnitCube u → ∀ t ∈ Ioo (0 : ℝ) 1,
          0 < dr n (sample r n u) t)
        (hA : ∀ u, InUnitCube u → diagonalProduct q dq N u = A)
        (hB : ∀ u, InUnitCube u → diagonalProduct r dr N u = B) :
        ∀ᵐ u ∂(Measure.pi fun _ : Fin N =>
          (volume : Measure ℝ).restrict (Ioo (0 : ℝ) 1)),
          geometricWeight q r dq dr N u = ENNReal.ofReal (Real.sqrt (A * B)) := by
    …

    Mentions: OAI.Problem358.TriangularDensity.InUnitCube, OAI.Problem358.TriangularDensity.diagonalProduct, OAI.Problem358.TriangularDensity.geometricWeight

16. theorem OAI.Problem358.TriangularDomination.weightedDomination_triangular_recursion line 292

    Source documentation

    Weighted substitution for every finite dimension from measurable triangular recursion and almost-everywhere one-dimensional fiber substitution. The maps and weights are supplied explicitly; no quantile existence is assumed implicitly.

    theorem weightedDomination_triangular_recursion
        (η : Measure ℝ) [SigmaFinite η]
        (F : (n : ℕ) → (Fin n → ℝ) → (Fin n → ℝ))
        (G : (n : ℕ) → ((Fin n → ℝ) × ℝ) → ℝ)
        (J : (n : ℕ) → (Fin n → ℝ) → ℝ≥0∞)
        (j : (n : ℕ) → ((Fin n → ℝ) × ℝ) → ℝ≥0∞)
        (hF : ∀ n, Measurable (F n)) (hG : ∀ n, Measurable (G n))
        (hJ : ∀ n, Measurable (J n)) (hj : ∀ n, Measurable (j n))
        (hzero : ∀ s, J 0 s = 1)
        (hrecursion : ∀ n s t,
          F (n + 1) (Fin.snoc s t) = Fin.snoc (F n s) (G n (s, t)))
        (hweight : ∀ n s t,
    …

17. theorem OAI.Problem358.TriangularDomination.weightedDomination_triangular_recursion_of_le line 343

    Source documentation

    Finite-cutoff version: no maps, derivatives, or substitution bounds beyond the requested ambient dimension need to satisfy any hypotheses.

    theorem weightedDomination_triangular_recursion_of_le
        (N : ℕ)
        (η : Measure ℝ) [SigmaFinite η]
        (F : (n : ℕ) → (Fin n → ℝ) → (Fin n → ℝ))
        (G : (n : ℕ) → ((Fin n → ℝ) × ℝ) → ℝ)
        (J : (n : ℕ) → (Fin n → ℝ) → ℝ≥0∞)
        (j : (n : ℕ) → ((Fin n → ℝ) × ℝ) → ℝ≥0∞)
        (hF : ∀ n, n ≤ N → Measurable (F n))
        (hG : ∀ n, n < N → Measurable (G n))
        (hJ : ∀ n, n ≤ N → Measurable (J n))
        (hj : ∀ n, n < N → Measurable (j n))
        (hzero : ∀ s, J 0 s = 1)
    …

18. theorem OAI.Problem358.TriangularDomination.WeightedDomination.midpoint_fiber line 410

    Source documentation

    Extend a weighted triangular change of variables by one midpoint coordinate. The fiber functions need derivatives only in their last variable, not in parameters.

    theorem WeightedDomination.midpoint_fiber
        {A B : Type*} [MeasurableSpace A] [MeasurableSpace B]
        {μ : Measure A} {ν : Measure B}
        {F : A → B} {J : A → ℝ≥0∞}
        {s : Set ℝ} {X Z X' Z' : A → ℝ → ℝ}
        (hs : MeasurableSet s) (hconv : Convex ℝ s)
        (hF : Measurable F) (hJ : Measurable J)
        (hX : Measurable (fun p : A × ℝ => X p.1 p.2))
        (hZ : Measurable (fun p : A × ℝ => Z p.1 p.2))
        (hX' : Measurable (fun p : A × ℝ => X' p.1 p.2))
        (hZ' : Measurable (fun p : A × ℝ => Z' p.1 p.2))
        (hderivX : ∀ a t, t ∈ s → HasDerivWithinAt (X a) (X' a t) s t)
    …

19. theorem OAI.Problem358.TriangularDomination.WeightedDomination.midpoint_fiber_smul_map_le line 443

    Source documentation

    The preceding induction step in the measure-domination form used by midpoint couplings, once the product weight has a uniform lower bound.

    theorem WeightedDomination.midpoint_fiber_smul_map_le
        {A B : Type*} [MeasurableSpace A] [MeasurableSpace B]
        {μ : Measure A} {ν : Measure B}
        {F : A → B} {J : A → ℝ≥0∞}
        {s : Set ℝ} {X Z X' Z' : A → ℝ → ℝ}
        (hs : MeasurableSet s) (hconv : Convex ℝ s)
        (hF : Measurable F) (hJ : Measurable J)
        (hX : Measurable (fun p : A × ℝ => X p.1 p.2))
        (hZ : Measurable (fun p : A × ℝ => Z p.1 p.2))
        (hX' : Measurable (fun p : A × ℝ => X' p.1 p.2))
        (hZ' : Measurable (fun p : A × ℝ => Z' p.1 p.2))
        (hderivX : ∀ a t, t ∈ s → HasDerivWithinAt (X a) (X' a t) s t)
    …

20. theorem OAI.Problem358.TriangularRecursion.measurable_midpoint_of_samples line 477

    Source documentation

    Measurability of the midpoint needs only the two samplers at the depth in question, not any conditional functions after that depth.

    theorem measurable_midpoint_of_samples (q r : ConditionalFamily) (n : ℕ)
        (hq : Measurable (sample q n)) (hr : Measurable (sample r n)) :
        Measurable (midpoint q r n) := by
    …

    Mentions: OAI.Problem358.TriangularRecursion.ConditionalFamily, OAI.Problem358.TriangularRecursion.sample, OAI.Problem358.TriangularRecursion.midpoint

21. theorem OAI.Problem358.TriangularRecursion.weightedDomination_midpoint_of_weight line 488

    Source documentation

    Specialization of finite triangular substitution to the canonical paired samplers. Regularity is needed only on sampled open-unit-cube prefixes. The recursive weight is the product of geometric means of longitudinal derivatives.

    theorem weightedDomination_midpoint_of_weight
        (q r dq dr : ConditionalFamily) (N : ℕ)
        (hq : ∀ n, n < N → Measurable (fun p : (Fin n → ℝ) × ℝ => q n p.1 p.2))
        (hr : ∀ n, n < N → Measurable (fun p : (Fin n → ℝ) × ℝ => r n p.1 p.2))
        (hdq : ∀ n, n < N → Measurable (fun p : (Fin n → ℝ) × ℝ => dq n p.1 p.2))
        (hdr : ∀ n, n < N → Measurable (fun p : (Fin n → ℝ) × ℝ => dr n p.1 p.2))
        (hsq : ∀ n, n ≤ N → Measurable (sample q n))
        (hsr : ∀ n, n ≤ N → Measurable (sample r n))
        (hderivq : ∀ n, n < N → ∀ s, InUnitCube s → ∀ t ∈ Ioo (0 : ℝ) 1,
          HasDerivAt (q n (sample q n s)) (dq n (sample q n s) t) t)
        (hderivr : ∀ n, n < N → ∀ s, InUnitCube s → ∀ t ∈ Ioo (0 : ℝ) 1,
          HasDerivAt (r n (sample r n s)) (dr n (sample r n s) t) t)
    …

    Mentions: OAI.Problem358.TriangularRecursion.ConditionalFamily, OAI.Problem358.TriangularRecursion.sample

22. theorem OAI.Problem358.TriangularRecursion.midpoint_smul_map_le_of_diagonalProducts line 541

    Source documentation

    Canonical finite-dimensional midpoint domination. The only quantitative input is the two constant terminal diagonal products; all weighted substitution and measurable-Jacobian conditions are discharged from the scalar data.

    theorem midpoint_smul_map_le_of_diagonalProducts
        (q r dq dr : ConditionalFamily) (N : ℕ) (A B : ℝ)
        (hq : ∀ n, n < N → Measurable (fun p : (Fin n → ℝ) × ℝ => q n p.1 p.2))
        (hr : ∀ n, n < N → Measurable (fun p : (Fin n → ℝ) × ℝ => r n p.1 p.2))
        (hdq : ∀ n, n < N → Measurable (fun p : (Fin n → ℝ) × ℝ => dq n p.1 p.2))
        (hdr : ∀ n, n < N → Measurable (fun p : (Fin n → ℝ) × ℝ => dr n p.1 p.2))
        (hsq : ∀ n, n ≤ N → Measurable (sample q n))
        (hsr : ∀ n, n ≤ N → Measurable (sample r n))
        (hderivq : ∀ n, n < N → ∀ s, InUnitCube s → ∀ t ∈ Ioo (0 : ℝ) 1,
          HasDerivAt (q n (sample q n s)) (dq n (sample q n s) t) t)
        (hderivr : ∀ n, n < N → ∀ s, InUnitCube s → ∀ t ∈ Ioo (0 : ℝ) 1,
          HasDerivAt (r n (sample r n s)) (dr n (sample r n s) t) t)
    …

    Mentions: OAI.Problem358.TriangularRecursion.ConditionalFamily, OAI.Problem358.TriangularRecursion.sample

23. def OAI.Problem358.TriangularDensity.densityRatio line 588

    Source documentation

    The derivative dictated by successive conditional section densities. It is defined on all prefixes, including invalid prefixes of density zero.

    def densityRatio (q : ConditionalFamily) (p : (n : ℕ) → Coordinates n → ℝ) :
        ConditionalFamily :=
    …

    Mentions: OAI.Problem358.TriangularDensity.Coordinates

24. theorem OAI.Problem358.TriangularDensity.measurable_densityRatio_of_le line 594

    Source documentation

    The ratio derivative field is jointly measurable using only the finite collection of section densities involved in the sampler.

    theorem measurable_densityRatio_of_le
        (q : ConditionalFamily) (p : (n : ℕ) → Coordinates n → ℝ) (N : ℕ)
        (hq : ∀ n, n < N → Measurable (fun z : Coordinates n × ℝ => q n z.1 z.2))
        (hp : ∀ n, n ≤ N → Measurable (p n)) :
        ∀ n, n < N → Measurable (fun z : Coordinates n × ℝ =>
          densityRatio q p n z.1 z.2) := by
    …

    Mentions: OAI.Problem358.TriangularDensity.Coordinates, OAI.Problem358.TriangularDensity.densityRatio

25. theorem OAI.Problem358.TriangularDensity.densityRatio_pos_on_sampled_prefixes line 608

    Source documentation

    Positivity of section densities propagates to the conditional derivative at every valid sampled prefix.

    theorem densityRatio_pos_on_sampled_prefixes
        (q : ConditionalFamily) (D : (n : ℕ) → Set (Coordinates n))
        (p : (n : ℕ) → Coordinates n → ℝ) (N : ℕ)
        (hzero : (fun i => Fin.elim0 i) ∈ D 0)
        (hstep : ∀ n, n < N → ∀ x, x ∈ D n → ∀ t ∈ Ioo (0 : ℝ) 1,
          Fin.snoc x (q n x t) ∈ D (n + 1))
        (hp : ∀ n, n ≤ N → ∀ x, x ∈ D n → 0 < p n x) :
        ∀ n, n < N → ∀ s, InUnitCube s → ∀ t ∈ Ioo (0 : ℝ) 1,
          0 < densityRatio q p n (sample q n s) t := by
    …

    Mentions: OAI.Problem358.TriangularDensity.Coordinates, OAI.Problem358.TriangularDensity.InUnitCube, OAI.Problem358.TriangularDensity.densityRatio

26. theorem OAI.Problem358.TriangularDensity.diagonalProduct_densityRatio_eq_initial line 624

    Source documentation

    Exact telescoping of the measurable ratio field, with the terminal density one on every valid terminal prefix.

    theorem diagonalProduct_densityRatio_eq_initial
        (q : ConditionalFamily) (D : (n : ℕ) → Set (Coordinates n))
        (p : (n : ℕ) → Coordinates n → ℝ) (N : ℕ)
        (hzero : (fun i => Fin.elim0 i) ∈ D 0)
        (hstep : ∀ n, n < N → ∀ x, x ∈ D n → ∀ t ∈ Ioo (0 : ℝ) 1,
          Fin.snoc x (q n x t) ∈ D (n + 1))
        (hp : ∀ n, n ≤ N → ∀ x, x ∈ D n → 0 < p n x)
        (hterminal : ∀ x ∈ D N, p N x = 1) :
        ∀ s, InUnitCube s → diagonalProduct q (densityRatio q p) N s =
          p 0 (fun i => Fin.elim0 i) := by
    …

    Mentions: OAI.Problem358.TriangularDensity.Coordinates, OAI.Problem358.TriangularDensity.InUnitCube, OAI.Problem358.TriangularDensity.diagonalProduct, OAI.Problem358.TriangularDensity.densityRatio

27. theorem OAI.Problem358.TriangularDensity.midpoint_smul_map_le_of_density_ratios line 640

    Source documentation

    For two geometric section-density families, positive conditional quantile derivatives and terminal density one imply the full midpoint domination. No independently measurable derivative field or Jacobian identity is required.

    theorem midpoint_smul_map_le_of_density_ratios
        (q r : ConditionalFamily) (D E : (n : ℕ) → Set (Coordinates n))
        (p v : (n : ℕ) → Coordinates n → ℝ) (N : ℕ)
        (hq : ∀ n, n < N → Measurable (fun z : Coordinates n × ℝ => q n z.1 z.2))
        (hr : ∀ n, n < N → Measurable (fun z : Coordinates n × ℝ => r n z.1 z.2))
        (hp : ∀ n, n ≤ N → Measurable (p n))
        (hv : ∀ n, n ≤ N → Measurable (v n))
        (hsq : ∀ n, n ≤ N → Measurable (sample q n))
        (hsr : ∀ n, n ≤ N → Measurable (sample r n))
        (hDzero : (fun i => Fin.elim0 i) ∈ D 0)
        (hEzero : (fun i => Fin.elim0 i) ∈ E 0)
        (hDstep : ∀ n, n < N → ∀ x, x ∈ D n → ∀ t ∈ Ioo (0 : ℝ) 1,
    …

    Mentions: OAI.Problem358.TriangularDensity.Coordinates