OneStepOddClassCornerTaylor

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

The two-point Taylor elimination, box-generic

The pointwise atom's (★) (OneStepEvenBound.abs_evenAffinePart_le_pointwise) is stated on the proved one-met-face slab/Taylor boxes. The corner pricing needs the same estimate on the window-hugging corner boxes of OneStepOddClassCornerGeometry, and — for the third application — at an affine competitor that is not a minimizer.

The estimate: for V odd about the met upper i-face, f = V − ℓ the residual against an arbitrary affine ℓ = affineEval (c − A·x) A, harmonic on T with Hessian bound M there, and y within depth delta of the face with y, ρᵢy, y − delta·eᵢ ∈ T:

  |evenᵢ(ℓ)(y)| ≤ 2|f y| + |f (y − delta·eᵢ)| + 3 M delta² .

The reflection identity f∘ρᵢ + f = −2·evenᵢ(ℓ) supplies the even part; the two second-order Taylor steps (towards the reflected and the pushed point) eliminate the unknown normal derivative.

References

• Adapted from OneStepEvenBound.abs_evenAffinePart_le_pointwise (same repository), the boxes abstracted.

8. Crude volume lower bounds

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.volume_toReal_coordBox_ge_of_edges {d : ℕ} {lo hi : Fin d → ℝ} {delta : ℝ} (hdelta : 0 < delta) (hedge : ∀ (l : Fin d), delta ≤ hi l - lo l) : delta ^ d ≤ (MeasureTheory.volume (coordBox lo hi)).toReal

Any box with all edges at least delta has volume at least delta^d.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.cornerFaceSlab_edge_ge {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} {i : Fin d} {delta : ℝ} (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hkm : k < m) (hdelta16 : 16 * delta ≤ 3 ^ k) (l : Fin d) : delta ≤ cornerFaceSlabHi x m k i l - cornerFaceSlabLo x m k i delta l

The face slab's edges are all at least delta.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.cornerPairSlab_edge_ge {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} {i j : Fin d} {delta : ℝ} (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hkm : k < m) (hdelta16 : 16 * delta ≤ 3 ^ k) (l : Fin d) : delta ≤ cornerPairSlabHi x m k i j l - cornerPairSlabLo x m k i j delta l

The corner slab's edges are all at least delta.

9. Face-depth accessors

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.cornerFaceSlab_depth {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} {i : Fin d} {delta : ℝ} {y : HCPolySupport.Vec d} (hy : y ∈ coordBox (cornerFaceSlabLo x m k i delta) (cornerFaceSlabHi x m k i)) : 1 / 2 * 3 ^ m - delta < y i ∧ y i < 1 / 2 * 3 ^ m

A point of the face slab is within delta of the met face.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.cornerPairSlab_depth {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} {i j : Fin d} {delta : ℝ} {y : HCPolySupport.Vec d} (hy : y ∈ coordBox (cornerPairSlabLo x m k i j delta) (cornerPairSlabHi x m k i j)) : (1 / 2 * 3 ^ m - delta < y i ∧ y i < 1 / 2 * 3 ^ m) ∧ 1 / 2 * 3 ^ m - delta < y j ∧ y j < 1 / 2 * 3 ^ m

A point of the corner slab is within delta of the j-face (and of the i-face).