ActualProjectionUnits.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The exact coefficient and forcing units of the actual projection

theorem OAI.RegularPointCoordinates.projection_coefficient_rescale line 17

Source documentation

Passing from the radius-weighted physical covector to the coefficient of the rescaled coordinates costs only the fixed radius ratio and frame norm.

theorem projection_coefficient_rescale {n : ℕ} (N : Euclidean n ≃L[ℝ] Euclidean n)
    {r M G alpha sigma : ℝ} (hr : 0 < r) (hN : ‖(N : Euclidean n →L[ℝ] Euclidean n)‖ ≤ M)
    (ell : Euclidean n) (k : ℝ)
    (hbound : |(r ^ 2)⁻¹ * k| + (r / 2048) * ‖N.symm ((r ^ 2)⁻¹ • ell)‖ ≤
      G * (alpha + sigma)) :
    ‖r⁻¹ • ell‖ + |(r ^ 2)⁻¹ * k| ≤
      max 1 (2048 * M) * G * (alpha + sigma) := by
…

Mentions: OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.sigma

theorem OAI.RegularPointCoordinates.radius_scaled_projection_euler_sum line 51

Source documentation

The rescaled Euler equation is exactly the finite-coordinate identity used by the published compactness theorem, including its constant term.

theorem radius_scaled_projection_euler_sum {n : ℕ} {r B B' : ℝ} (hr : 0 < r)
    (Ω : Set X) (hfin : μ Ω ≠ ∞) (u : Fin n → SobolevSpace μ hQ)
    (f w eta e : SobolevSpace μ hQ) (ell : Euclidean n) (k : ℝ)
    (heta : SobolevSpace.toLp μ hQ eta =ᵐ[μ.restrict Ω] fun _ => (1 : ℝ))
    (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 + sobolevColumnMap μ hQ u ell + k • eta + e)) :
    r ^ 2 • localRadialDerivative μ hQ Ω ((r ^ 2)⁻¹ • f) hf' ((r ^ 2)⁻¹ • w) =
      SobolevSpace.restrictLp μ hQ Ω ((r ^ 2)⁻¹ • w) +
      (∑ j, (r⁻¹ • ell) j • SobolevSpace.restrictLp μ hQ Ω (radiusScaledColumns μ hQ r u j)) +
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.localRadialDerivative, OAI.RegularPointCoordinates.SobolevSpace.restrictLp, OAI.RegularPointCoordinates.sobolevColumnMap, OAI.RegularPointCoordinates.radiusScaledColumns

theorem OAI.RegularPointCoordinates.normalized_sobolev_norm_congr line 73
Source documentation
A mean-square norm is unchanged when only the proof of finiteness or the presentation of the same measurable set changes.
```
theorem normalized_sobolev_norm_congr {s t : Set X} (hst : s = t)
    (hs : μ s ≠ ∞) (ht : μ t ≠ ∞) (w : SobolevSpace μ hQ) :
    ‖normalizeLocalL2 μ s hs (SobolevSpace.restrictLp μ hQ s w)‖ =
      ‖normalizeLocalL2 μ t ht (SobolevSpace.restrictLp μ hQ t w)‖ := by
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.normalizeLocalL2, OAI.RegularPointCoordinates.SobolevSpace.restrictLp