PinchingPairingRestriction.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The actual direction pairings in the small mass-test frame

theorem OAI.RegularPointCoordinates.uncentered_frame_normalization line 21

Source documentation

Removing the local constant does not change the exact frame used by full-mass pinching. Both frame changes act on the original coordinate map.

theorem uncentered_frame_normalization {n : ℕ}
    (u : Fin n → SobolevSpace μ hQ) (eta : SobolevSpace μ hQ) (z : Euclidean n)
    (F N : Euclidean n ≃L[ℝ] Euclidean n) (Ω : Set X) (hΩ : MeasurableSet Ω)
    (heta : SobolevSpace.toLp μ hQ eta =ᵐ[μ.restrict Ω] fun _ => (1 : ℝ))
    (hN : IsExactMeanNormalization μ hQ
      ((centeredSobolevMap μ hQ u eta z).comp F.toContinuousLinearMap) Ω hΩ N) :
    sobolevMeanGram μ hQ ((sobolevColumnMap μ hQ u).comp
      (F.toContinuousLinearMap.comp N.toContinuousLinearMap)) Ω hΩ =
      ContinuousLinearMap.id ℝ (Euclidean n) := by
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.IsExactMeanNormalization, OAI.RegularPointCoordinates.centeredSobolevMap, OAI.RegularPointCoordinates.sobolevMeanGram, OAI.RegularPointCoordinates.sobolevColumnMap

theorem OAI.RegularPointCoordinates.pinching_pairing_restrict line 40

Source documentation

Restriction and a bounded exact frame preserve the actual constant pairing, with only the square root of the volume loss.

theorem pinching_pairing_restrict {n : ℕ} {Ω Ω' : Set X} (hsub : Ω' ⊆ Ω)
    (hfin : μ Ω ≠ ∞) (hfin' : μ Ω' ≠ ∞)
    (hpos : 0 < μ.real Ω) (hpos' : 0 < μ.real Ω')
    (eta : SobolevSpace μ hQ)
    (heta : SobolevSpace.toLp μ hQ eta =ᵐ[μ.restrict Ω'] fun _ => (1 : ℝ))
    (G : Euclidean n →L[ℝ] SobolevSpace μ hQ) (delta : Euclidean n)
    (N : Euclidean n ≃L[ℝ] Euclidean n) (hN : ‖N.toContinuousLinearMap‖ ≤ 2)
    {C D : ℝ} (hC : 0 ≤ C) (hD : 0 ≤ D) (hvol : μ.real Ω ≤ C * μ.real Ω')
    (hfit : ∀ b, ‖normalizeLocalL2 μ Ω hfin
      (SobolevSpace.restrictLp μ hQ Ω (G b - ⟪delta, b⟫_ℝ • eta))‖ ≤ D * ‖b‖) :
    ∀ b, ‖normalizeLocalL2 μ Ω' hfin'
      (SobolevSpace.restrictLp μ hQ Ω' ((G.comp N.toContinuousLinearMap) b) -
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.normalizeLocalL2, OAI.RegularPointCoordinates.SobolevSpace.restrictLp