OAI/Analysis/Mahler/StripVolume.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SymmetricMahler.stripSublevel line 13
2. lemma OAI.SymmetricMahler.isOpen_stripDomain line 16
3. lemma OAI.SymmetricMahler.continuousOn_stripTau line 23
4. lemma OAI.SymmetricMahler.isOpen_stripSublevel line 42
5. def OAI.SymmetricMahler.stripHessianDet line 46
6. theorem OAI.SymmetricMahler.stripMap_volume_eq line 54

   Source documentation

   Change of variables for the literal finite-strip map, allowing vanishing Jacobian values. Neither local invertibility nor a change-of-variables premise is assumed.

   theorem stripMap_volume_eq (A : Matrix (Fin N) (Fin n) ℝ)
       (hA : Function.Injective (measurement A)) {m : ℕ} (hm : 2 ≤ m) :
       volume (stripMap A m '' stripSublevel A m) =
         ∫⁻ z in stripSublevel A m,
           ENNReal.ofReal ((4/(Real.pi*(m : ℝ)))^n*stripHessianDet A m z) := by
   …

   Mentions: OAI.SymmetricMahler.measurement, OAI.SymmetricMahler.stripMap, OAI.SymmetricMahler.stripSublevel, OAI.SymmetricMahler.stripHessianDet

7. theorem OAI.SymmetricMahler.stripMap_image_subset_product line 75

   Source documentation

   Pointwise containment in K times a scaled polar body.

   theorem stripMap_image_subset_product (A : Matrix (Fin N) (Fin n) ℝ)
       {m : ℕ} (hm : 2 ≤ m) :
       stripMap A m '' stripSublevel A m ⊆ stripBody A ×ˢ
         ((1+(N : ℝ)*planarError m) • coordinatePolar (stripBody A)) := by
   …

   Mentions: OAI.SymmetricMahler.stripMap, OAI.SymmetricMahler.stripSublevel, OAI.SymmetricMahler.stripBody, OAI.SymmetricMahler.planarError, OAI.SymmetricMahler.coordinatePolar

8. theorem OAI.SymmetricMahler.stripMap_volume_le_product line 91

   Source documentation

   The image-volume upper bound from the actual polar containment.

   theorem stripMap_volume_le_product (A : Matrix (Fin N) (Fin n) ℝ)
       {m : ℕ} (hm : 2 ≤ m) :
       volume (stripMap A m '' stripSublevel A m) ≤
         volume (stripBody A) * (ENNReal.ofReal ((1+(N : ℝ)*planarError m)^n)*
           volume (coordinatePolar (stripBody A))) := by
   …

   Mentions: OAI.SymmetricMahler.stripMap, OAI.SymmetricMahler.stripSublevel, OAI.SymmetricMahler.stripBody, OAI.SymmetricMahler.planarError, OAI.SymmetricMahler.coordinatePolar