OAI/Analysis/Mahler/SourceCoordinateForms.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Mahler.sourceBoundarySlots line 13

   Source documentation

   The leading one-form slot precedes the interleaved two-form slots.

   def sourceBoundarySlots (k : ℕ) : Fin 1 ⊕ WedgePowerSlots k ≃ Fin (2*k+1) :=
   …

   Mentions: OAI.Mahler.WedgePowerSlots

2. def OAI.Mahler.sourceReindex line 20
3. def OAI.Mahler.sourceReindexCLM line 24
4. def OAI.Mahler.sourceRealBoundaryForm line 32
5. lemma OAI.Mahler.sourceRealBoundaryForm_apply line 38
6. lemma OAI.Mahler.contDiffAt_sourceRealBoundaryForm line 43
7. def OAI.Mahler.sourceCoordinateForm line 51
8. lemma OAI.Mahler.contDiffAt_sourceCoordinateForm line 56
9. theorem OAI.Mahler.MassHypotheses.contDiffOn_coordinateEnergy line 66
10. theorem OAI.Mahler.MassHypotheses.contDiffOn_coordinateLog line 72
11. theorem OAI.Mahler.sourceCoordinateForm_regular_face line 84

    Source documentation

    The level equation holds on the open chart-face domain; this theorem applies the full R^(-(k+1)) law to the real Stokes form.

    theorem sourceCoordinateForm_regular_face {d : ℕ}
        (h : MassHypotheses n N m U f G)
        (Ψ : (Fin (d+1) → ℝ) ≃L[ℝ] ComplexEuclidean n)
        (p : MahlerStokes.RegularBoundaryPatch (d+1) (Ψ ⁻¹' U) (fun x => tau f (Ψ x)))
        {R : ℝ} (hR : 0 < R) {y : Fin d → ℝ} (hy : y ∈ p.faceDomain R) (k : ℕ) :
        MahlerStokes.pullbackForm (p.faceParam R) (sourceCoordinateForm Ψ (logTau f) k) y =
          (R⁻¹)^(k+1) •
            MahlerStokes.pullbackForm (p.faceParam R) (sourceCoordinateForm Ψ (energy f) k) y := by
    …

    Mentions: OAI.Mahler.MassHypotheses, OAI.Mahler.ComplexEuclidean, OAI.MahlerStokes.RegularBoundaryPatch, OAI.Mahler.tau, OAI.MahlerStokes.pullbackForm, OAI.Mahler.sourceCoordinateForm, OAI.Mahler.logTau, OAI.Mahler.energy