OverlappingExactFrames.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Comparing two exact frames through their common overlap

theorem OAI.RegularPointCoordinates.overlap_square_comparison line 13

theorem OAI.RegularPointCoordinates.overlapping_exact_frames line 25

Source documentation

The same positive overlap compares exact normalizers centered at two points. Only the already controlled volume-ratio loss enters the bound.

theorem overlapping_exact_frames {n : ℕ}
    (u : Fin n → SobolevSpace μ hQ) (p q : X) (R : ℝ)
    (Np Nq : Euclidean n ≃L[ℝ] Euclidean n) {ε C : ℝ}
    (hε : 0 ≤ ε) (hC : 0 ≤ C) (hsmall : (n : ℝ) ^ 2 * (C * ε) ≤ 1 / 3)
    (vp vq : X → Euclidean n)
    (hp : FirstOrderSplittingOn μ hQ p R ε (transformedColumn μ hQ u Np) vp)
    (hq : FirstOrderSplittingOn μ hQ q R ε (transformedColumn μ hQ u Nq) vq)
    (hep : IsExactMeanNormalization μ hQ (sobolevColumnMap μ hQ u) (ball p R) measurableSet_ball Np)
    (heq : IsExactMeanNormalization μ hQ (sobolevColumnMap μ hQ u) (ball q R) measurableSet_ball Nq)
    (S : Set X) (hS : MeasurableSet S) (hSp : S ⊆ ball p R) (hSq : S ⊆ ball q R)
    (hS0 : μ S ≠ 0) (hSfin : μ S ≠ ∞)
    (hp0 : μ (ball p R) ≠ 0) (hpfin : μ (ball p R) ≠ ∞)
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.FirstOrderSplittingOn, OAI.RegularPointCoordinates.transformedColumn, OAI.RegularPointCoordinates.IsExactMeanNormalization, OAI.RegularPointCoordinates.sobolevColumnMap