OAI/Analysis/Mahler/SphereRadius.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MahlerStokes.smul_coordBall_unit line 10
2. theorem OAI.MahlerStokes.setIntegral_coordBall_scale line 26

   Source documentation

   Positive dilation of the actual coordinate Lebesgue integral.

   theorem setIntegral_coordBall_scale {n : ℕ} {r : ℝ} (hr : 0 < r)
       (f : (Fin n → ℝ) → ℝ) :
       (∫ y in coordBall n r, f y) = r^n * ∫ x in coordBall n 1, f (r • x) := by
   …

   Mentions: OAI.MahlerStokes.coordBall

3. lemma OAI.MahlerStokes.chord_pos_scale line 43
4. lemma OAI.MahlerStokes.insertNth_smul_boundary line 50
5. theorem OAI.MahlerStokes.sphereFlux_pos_scale line 60

   Source documentation

   Radius scaling of the coordinate sphere flux, without exterior algebra or flux-form identities.

   theorem sphereFlux_pos_scale {n : ℕ} {r : ℝ} (hr : 0 < r)
       (ω : (Fin (n+1) → ℝ) → (Fin (n+1) → ℝ) [⋀^Fin n]→L[ℝ] ℝ) :
       sphereFlux r ω = r^n * sphereFlux 1 (fun x => ω (r • x)) := by
   …

   Mentions: OAI.MahlerStokes.sphereFlux