OAI/Analysis/Mahler/SpecialMassBridge.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SymmetricMahler.specialGramDet line 13

   Source documentation

   Real determinant of the actual holomorphic derivative's Hermitian Gram matrix.

   noncomputable def specialGramDet (A : Matrix (Fin N) (Fin n) ℝ) (m : ℕ) (z : Fin n → ℂ) : ℝ :=
   …

2. lemma OAI.SymmetricMahler.specialGramDet_eq_stripHessianDet line 16
3. def OAI.SymmetricMahler.specialSublevel line 27
4. lemma OAI.SymmetricMahler.specialSublevel_eq_preimage line 30
5. lemma OAI.SymmetricMahler.measurableEmbedding_complexToReal line 36
6. theorem OAI.SymmetricMahler.specialGram_integral_eq line 39
7. theorem OAI.SymmetricMahler.stripMassBound_of_special_gram_mass line 50

   Source documentation

   The n! factor converts the complex mass inequality into the mass premise for the finite-strip reduction.

   theorem stripMassBound_of_special_gram_mass (A : Matrix (Fin N) (Fin n) ℝ)
       {m : ℕ} (hm : 2 ≤ m)
       (hmass : ENNReal.ofReal ((Real.pi*(m : ℝ))^n) ≤
         ∫⁻ z in specialSublevel A m, ENNReal.ofReal ((Nat.factorial n : ℝ)*specialGramDet A m z)) :
       StripMassBound A m := by
   …

   Mentions: OAI.SymmetricMahler.specialSublevel, OAI.SymmetricMahler.specialGramDet, OAI.SymmetricMahler.StripMassBound