OAI/Analysis/Mahler/SourceFluxRegularity.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Mahler.sourceDCOperator line 15

   Source documentation

   Linear jet operator for the normalization -D(u)(iv)/4.

   def sourceDCOperator : (E →L[ℝ] ℂ) →L[ℝ] E [⋀^Fin 1]→L[ℝ] ℂ :=
   …

2. lemma OAI.Mahler.contDiffAt_sourceDC line 20
3. lemma OAI.Mahler.contDiffAt_sourceDDC line 25
4. def OAI.Mahler.continuousWedgePower line 35

   Source documentation

   The recursive shuffle power as a continuous form.

   def continuousWedgePower (a : E [⋀^Fin 2]→L[ℝ] ℂ) :
       (k : ℕ) → E [⋀^WedgePowerSlots k]→L[ℝ] ℂ
     | 0 => ContinuousAlternatingMap.constOfIsEmpty ℝ E (Fin 0) 1
     | k+1 => continuousWedge a (continuousWedgePower a k)
   
   omit [NormedSpace ℂ E] [IsScalarTower ℝ ℂ E] [FiniteDimensional ℝ E] in

   Mentions: OAI.Mahler.WedgePowerSlots, OAI.Mahler.continuousWedge

5. lemma OAI.Mahler.continuousWedgePower_toAlternatingMap line 41
6. lemma OAI.Mahler.contDiffAt_continuousWedgePower line 48
7. def OAI.Mahler.continuousSourceBoundaryForm line 56
8. lemma OAI.Mahler.continuousSourceBoundaryForm_eq line 61
9. lemma OAI.Mahler.continuousSourceBoundaryForm_apply line 68
10. theorem OAI.Mahler.contDiffAt_sourceBoundaryForm line 74

    Source documentation

    C1 regularity of the whole actual flux form uses C3 of its potential.

    theorem contDiffAt_sourceBoundaryForm {u : E → ℂ} {x : E}
        (hu : ContDiffAt ℝ 3 u x) (k : ℕ) :
        ContDiffAt ℝ 1 (continuousSourceBoundaryForm u k) x := by
    …

    Mentions: OAI.Mahler.continuousSourceBoundaryForm

11. theorem OAI.Mahler.MassHypotheses.contDiffOn_energyBoundaryForm line 85
12. theorem OAI.Mahler.MassHypotheses.contDiffOn_logBoundaryForm line 90