RescaledRadialFunction.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Exact radial and amplitude rescaling in the compactness argument

theorem OAI.RegularPointCoordinates.rescaled_radial_laplacian line 20
Source documentation
A constant source rescales in the original weak equation.
```
theorem rescaled_radial_laplacian (Ω : Set X) (f : SobolevSpace μ hQ) {r c : ℝ}
    (hf : IsConstantLaplacianOn μ hQ Ω f c) :
    IsConstantLaplacianOn μ hQ Ω ((r ^ 2)⁻¹ • f) (c / r ^ 2) := by
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.IsConstantLaplacianOn

theorem OAI.RegularPointCoordinates.rescaled_radial_value line 27

Source documentation

The physical quadratic value bound becomes a dimensionless bound.

theorem rescaled_radial_value (Ω : Set X) (f : SobolevSpace μ hQ) {r A : ℝ}
    (hr : 0 < r)
    (hf : ∀ᵐ x ∂μ.restrict Ω, |SobolevSpace.toLp μ hQ f x| ≤ A * r ^ 2) :
    ∀ᵐ x ∂μ.restrict Ω, |SobolevSpace.toLp μ hQ ((r ^ 2)⁻¹ • f) x| ≤ A := by
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.SobolevSpace.toLp

theorem OAI.RegularPointCoordinates.rescaled_radial_energy line 41

Source documentation

The same radial rescaling has uniformly bounded dimensionless energy.

theorem rescaled_radial_energy (Ω : Set X) (f : SobolevSpace μ hQ) {r B : ℝ}
    (hr : 0 < r)
    (hf : ∀ᵐ x ∂μ.restrict Ω, localGamma μ hQ f f x ≤ B * r ^ 2) :
    ∀ᵐ x ∂μ.restrict Ω,
      r ^ 2 * localGamma μ hQ ((r ^ 2)⁻¹ • f) ((r ^ 2)⁻¹ • f) x ≤ B := by
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.localGamma

theorem OAI.RegularPointCoordinates.rescaled_radial_derivative line 60

Source documentation

The derivative with respect to the rescaled radial function, multiplied by the metric scaling factor, is exactly the original radial derivative.

theorem rescaled_radial_derivative (Ω : Set X) (f w : SobolevSpace μ hQ) {r B B' : ℝ}
    (hr : 0 < r)
    (hf : ∀ᵐ x ∂μ.restrict Ω, localGamma μ hQ f f x ≤ B)
    (hf' : ∀ᵐ x ∂μ.restrict Ω,
      localGamma μ hQ ((r ^ 2)⁻¹ • f) ((r ^ 2)⁻¹ • f) x ≤ B') :
    r ^ 2 • localRadialDerivative μ hQ Ω ((r ^ 2)⁻¹ • f) hf' w =
      localRadialDerivative μ hQ Ω f hf w := by
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.localRadialDerivative

theorem OAI.RegularPointCoordinates.rescaled_projected_euler_identity line 78

Source documentation

Both changes of scale in the projected Euler equation are exact. The coefficient and forcing scalings are made explicit.

theorem rescaled_projected_euler_identity {n : ℕ} (Ω : Set X) (hfin : μ Ω ≠ ∞)
    (f w e : SobolevSpace μ hQ) (u : Fin n → SobolevSpace μ hQ)
    (b : Fin n → ℝ) (k a : ℝ) {r B B' : ℝ} (hr : 0 < r)
    (hf : ∀ᵐ x ∂μ.restrict Ω, localGamma μ hQ f f x ≤ B)
    (hf' : ∀ᵐ x ∂μ.restrict Ω,
      localGamma μ hQ ((r ^ 2)⁻¹ • f) ((r ^ 2)⁻¹ • f) x ≤ B')
    (hid : localRadialDerivative μ hQ Ω f hf w =
      SobolevSpace.restrictLp μ hQ Ω w + (∑ j, b j • SobolevSpace.restrictLp μ hQ Ω (u j)) +
      k • restrictedOne μ Ω hfin + SobolevSpace.restrictLp μ hQ Ω e) :
    r ^ 2 • localRadialDerivative μ hQ Ω ((r ^ 2)⁻¹ • f) hf' (a • w) =
      SobolevSpace.restrictLp μ hQ Ω (a • w) +
      (∑ j, (a * b j) • SobolevSpace.restrictLp μ hQ Ω (u j)) +
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.localRadialDerivative, OAI.RegularPointCoordinates.SobolevSpace.restrictLp, OAI.RegularPointCoordinates.restrictedOne