OAI/Analysis/Mahler/SourceBoundaryIntegral.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Mahler.chartBoundaryFlux_source_scaling line 15

   Source documentation

   The R^(-(k+1)) boundary restriction survives the actual oriented chart integral, including its compact cutoff and its zero extension.

   theorem chartBoundaryFlux_source_scaling (h : MassHypotheses n N m U f G) (k : ℕ)
       (Ψ : (Fin ((2*k+1)+1) → ℝ) ≃L[ℝ] ComplexEuclidean n)
       (p : RegularBoundaryPatch ((2*k+1)+1) (Ψ ⁻¹' U) (fun x => tau f (Ψ x)))
       {R : ℝ} (hR : 0 < R) (ρ : (Fin ((2*k+1)+1) → ℝ) → ℝ)
       (hρ : tsupport ρ ⊆ p.domain) :
       chartBoundaryFlux p.chart p.coordinate R (fun z => ρ z • sourceCoordinateForm Ψ (logTau f) k z) =
         (R⁻¹)^(k+1) * chartBoundaryFlux p.chart p.coordinate R
           (fun z => ρ z • sourceCoordinateForm Ψ (energy f) k z) := by
   …

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

2. theorem OAI.Mahler.source_punctured_scaled_extDeriv line 60

   Source documentation

   The Stokes identity for coordinate flux forms, with all charts eliminated from the conclusion. The volume integrands are exterior derivatives of those forms; equality to Hessian top powers is not asserted by this theorem.

   theorem source_punctured_scaled_extDeriv (h : MassHypotheses n N m U f G) (k : ℕ)
       (Ψ : (Fin ((2*k+1)+1) → ℝ) ≃L[ℝ] ComplexEuclidean n)
       {R r : ℝ} (hR : 0 < R) (hR1 : R < 1)
       (hreg : ∀ x ∈ U, tau f x = R → fderiv ℝ (tau f) x ≠ 0)
       (hr : 0 < r)
       (hB : coordClosedBall ((2*k+1)+1) r ⊆ regularSublevel (Ψ ⁻¹' U) (fun x => tau f (Ψ x)) R) :
       (R⁻¹)^(k+1) *
         (∫ x in regularSublevel (Ψ ⁻¹' U) (fun x => tau f (Ψ x)) R,
           extDeriv (sourceCoordinateForm Ψ (energy f) k) x (coordinateBasis ((2*k+1)+1))) -
         sphereFlux r (sourceCoordinateForm Ψ (logTau f) k) =
         ∫ x in regularSublevel (Ψ ⁻¹' U) (fun x => tau f (Ψ x)) R \ coordClosedBall ((2*k+1)+1) r,
           extDeriv (sourceCoordinateForm Ψ (logTau f) k) x (coordinateBasis ((2*k+1)+1)) := by
   …

   Mentions: OAI.Mahler.MassHypotheses, OAI.Mahler.ComplexEuclidean, OAI.Mahler.tau, OAI.Mahler.sourceCoordinateForm, OAI.Mahler.energy, OAI.Mahler.sphereFlux, OAI.Mahler.logTau