OAI/Analysis/Mahler/ReferenceSphere.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Mahler.level_oneForm_scaling line 15

   Source documentation

   Restriction to any linear space of vectors tangent to an energy level.

   theorem level_oneForm_scaling {f : ι → E → ℂ} {U : Set E} {x : E}
       (hU : IsOpen U) (hx : x ∈ U) (hf : ∀ j, DifferentiableOn ℂ (f j) U)
       (ht : 0 < tau f x) (S : Submodule ℝ E) :
       (oneForm (dcLinear (logTau f)) x).toAlternatingMap.compLinearMap S.subtype =
         (energy f x)⁻¹ •
           (oneForm (dcLinear (energy f)) x).toAlternatingMap.compLinearMap S.subtype := by
   …

   Mentions: OAI.Mahler.tau, OAI.Mahler.oneForm, OAI.Mahler.dcLinear, OAI.Mahler.logTau, OAI.Mahler.energy

2. theorem OAI.Mahler.level_twoForm_scaling line 27
3. theorem OAI.Mahler.level_boundaryForm_scaling line 44

   Source documentation

   The complete boundary form scales by tau^(-(k+1)), with the actual shuffle exterior power. No integration identity is assumed.

   theorem level_boundaryForm_scaling {f : ι → E → ℂ} {U : Set E} {x : E}
       (hU : IsOpen U) (hx : x ∈ U) (hf : ∀ j, DifferentiableOn ℂ (f j) U)
       (ht : 0 < tau f x) (S : Submodule ℝ E)
       (hS : ∀ v : S, fderiv ℝ (energy f) x v = 0) (k : ℕ) :
       wedge ((oneForm (dcLinear (logTau f)) x).toAlternatingMap.compLinearMap S.subtype)
         (wedgePower ((extDeriv (oneForm (dcLinear (logTau f))) x).toAlternatingMap.compLinearMap S.subtype) k) =
       ((energy f x)⁻¹) ^ (k+1) •
         wedge ((oneForm (dcLinear (energy f)) x).toAlternatingMap.compLinearMap S.subtype)
           (wedgePower ((extDeriv (oneForm (dcLinear (energy f))) x).toAlternatingMap.compLinearMap S.subtype) k) := by
   …

   Mentions: OAI.Mahler.tau, OAI.Mahler.energy, OAI.Mahler.wedge, OAI.Mahler.oneForm, OAI.Mahler.dcLinear, OAI.Mahler.logTau, OAI.Mahler.wedgePower

4. lemma OAI.Mahler.coordinateMap_energy line 56
5. lemma OAI.Mahler.normEnergy_fderiv line 62
6. lemma OAI.Mahler.normEnergy_sphere_tangent line 69
7. theorem OAI.Mahler.reference_sphere_boundaryForm line 78

   Source documentation

   The reference logarithmic boundary form equals the actual squared-norm boundary form on the unit sphere, in every exterior degree.

   theorem reference_sphere_boundaryForm {n : ℕ} {z : ComplexEuclidean n}
       (hz : ‖z‖ = 1) (k : ℕ) :
       wedge (tangentForm z (oneForm (dcLinear (logTau (coordinateMap n))) z).toAlternatingMap)
         (wedgePower (tangentForm z
           (extDeriv (oneForm (dcLinear (logTau (coordinateMap n)))) z).toAlternatingMap) k) =
       wedge (tangentForm z (oneForm (dcLinear (normEnergy n)) z).toAlternatingMap)
         (wedgePower (tangentForm z
           (extDeriv (oneForm (dcLinear (normEnergy n))) z).toAlternatingMap) k) := by
   …

   Mentions: OAI.Mahler.ComplexEuclidean, OAI.Mahler.wedge, OAI.Mahler.tangentForm, OAI.Mahler.oneForm, OAI.Mahler.dcLinear, OAI.Mahler.logTau, OAI.Mahler.coordinateMap, OAI.Mahler.wedgePower, OAI.Mahler.normEnergy