Coarse-graining support:

Support.Deterministic.ConstantCoefficientDirichletBesov.StandardProjectionIncrementEnergy

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Energy bounds for standard martingale increments

This file records the local Jensen step needed for the boundary-budget construction: a child-minus-parent average is controlled by the L² energy of the field measured relative to the parent average on that child.

theorem HCPolySupport.vecNormSq_childAverage_sub_parentAverage_le_sum_cubeAverage_sq_sub_parentAverage {d : ℕ} {T R : TriadicCube d} (u : Vec d → Vec d) (_hRT : R ∈ childCubes T) (huR : MeasureTheory.MemLp u 2 (normalizedCubeMeasure R)) : vecNormSq (cubeAverageVec R u - cubeAverageVec T u) ≤ ∑ i : Fin d, cubeAverage R fun (x : Vec d) => (u x i - cubeAverageVec T u i) ^ 2

A child-average jump is controlled coordinatewise by the child L² energy relative to the parent average.

theorem HCPolySupport.vecNormSq_cubeIncrementVec_le_sum_cubeAverage_sq_sub_parentAverage {d : ℕ} {Q T R : TriadicCube d} {m : ℕ} (u : Vec d → Vec d) (hT : T ∈ descendantsAtDepth Q m) (hRT : R ∈ childCubes T) {x : Vec d} (hxR : x ∈ cubeSet R) (huR : MeasureTheory.MemLp u 2 (normalizedCubeMeasure R)) : vecNormSq (cubeIncrementVec Q (m + 1) u x) ≤ ∑ i : Fin d, cubeAverage R fun (y : Vec d) => (u y i - cubeAverageVec T u i) ^ 2

Pointwise form for a martingale increment on a child cube: the squared increment value is paid by the child energy relative to the parent average.

theorem HCPolySupport.cubeAverage_sq_sub_parentAverage_nonneg {d : ℕ} (T R : TriadicCube d) (u : Vec d → Vec d) (i : Fin d) : 0 ≤ cubeAverage R fun (y : Vec d) => (u y i - cubeAverageVec T u i) ^ 2

theorem HCPolySupport.childEnergy_sum_nonneg {d : ℕ} (T R : TriadicCube d) (u : Vec d → Vec d) : 0 ≤ ∑ i : Fin d, cubeAverage R fun (y : Vec d) => (u y i - cubeAverageVec T u i) ^ 2

theorem HCPolySupport.parentChildEnergy_sum_nonneg {d : ℕ} (T : TriadicCube d) (u : Vec d → Vec d) : 0 ≤ ∑ R ∈ childCubes T, ∑ i : Fin d, cubeAverage R fun (y : Vec d) => (u y i - cubeAverageVec T u i) ^ 2

theorem HCPolySupport.parentChildEnergy_sum_le_card_mul_cubeLpNorm_cubeFluctuationVec_sq {d : ℕ} (T : TriadicCube d) (u : Vec d → Vec d) (huT : MeasureTheory.MemLp u 2 (normalizedCubeMeasure T)) : (∑ R ∈ childCubes T, ∑ i : Fin d, cubeAverage R fun (y : Vec d) => (u y i - cubeAverageVec T u i) ^ 2) ≤ 3 ^ d * ↑(Fintype.card (Fin d)) * cubeLpNorm T 2 (cubeFluctuationVec T u) ^ 2

The child-energy sum relative to a parent average is controlled by the ordinary vector L² fluctuation on the parent. The factor 3^d comes from summing normalized child averages rather than averaging over the children, and the factor d comes from comparing the Euclidean coordinate sum to the ambient Pi norm used by cubeLpNorm.

theorem HCPolySupport.parentChildEnergy_sum_descendants_le_const_mul_depthAverage {d : ℕ} (Q : TriadicCube d) (u : Vec d → Vec d) (m : ℕ) (huParent : ∀ T ∈ descendantsAtDepth Q m, MeasureTheory.MemLp u 2 (normalizedCubeMeasure T)) : (∑ T ∈ descendantsAtDepth Q m, ∑ R ∈ childCubes T, ∑ i : Fin d, cubeAverage R fun (y : Vec d) => (u y i - cubeAverageVec T u i) ^ 2) ≤ 3 ^ d * ↑(Fintype.card (Fin d)) * ↑(descendantsAtDepth Q m).card * cubeBesovPositiveVectorDepthAverage Q u m

Summed over all depth-m parents, the parent child-energy budgets are controlled by the ordinary standard positive depth average.

theorem HCPolySupport.vecNormSq_cubeIncrementVec_le_childEnergy_sum_of_mem_parent {d : ℕ} {Q T : TriadicCube d} {m : ℕ} (u : Vec d → Vec d) (hT : T ∈ descendantsAtDepth Q m) {x : Vec d} (hxT : x ∈ cubeSet T) (huChild : ∀ R ∈ childCubes T, MeasureTheory.MemLp u 2 (normalizedCubeMeasure R)) : vecNormSq (cubeIncrementVec Q (m + 1) u x) ≤ ∑ R ∈ childCubes T, ∑ i : Fin d, cubeAverage R fun (y : Vec d) => (u y i - cubeAverageVec T u i) ^ 2

If the point lies in a depth-m parent, the pointwise martingale increment at scale m + 1 is controlled by the finite sum of the child energies of that parent.

theorem HCPolySupport.sq_overlapCubeLpNorm_overlapCubeFluctuationVec_cubeIncrementVec_le_four_mul_childEnergy_sum {d : ℕ} {Q T S : TriadicCube d} {m : ℕ} (u : Vec d → Vec d) (hT : T ∈ descendantsAtDepth Q m) (hsub : overlapCubeSet S ⊆ cubeSet T) (hinc : MeasureTheory.MemLp (cubeIncrementVec Q (m + 1) u) 2 (normalizedOverlapCubeMeasure S)) (huChild : ∀ R ∈ childCubes T, MeasureTheory.MemLp u 2 (normalizedCubeMeasure R)) : overlapCubeLpNorm S 2 (overlapCubeFluctuationVec S (cubeIncrementVec Q (m + 1) u)) ^ 2 ≤ 4 * ∑ R ∈ childCubes T, ∑ i : Fin d, cubeAverage R fun (y : Vec d) => (u y i - cubeAverageVec T u i) ^ 2

Local overlap version of the child-energy budget. When the overlap cube does not leave a depth-m parent, the fluctuation of the m + 1 martingale increment is paid by the finite child-energy sum of that parent.

noncomputable def HCPolySupport.overlapIntersectingParentsAtDepth {d : ℕ} (Q S : TriadicCube d) (m : ℕ) : Finset (TriadicCube d)

Depth-m parents whose standard cubes meet a fixed overlap cube. This is the local-neighbor family needed for the true finite-overlap summation.

Equations

• HCPolySupport.overlapIntersectingParentsAtDepth Q S m = {T ∈ HCPolySupport.descendantsAtDepth Q m | (HCPolySupport.overlapCubeSet S ∩ HCPolySupport.cubeSet T).Nonempty}

theorem HCPolySupport.mem_overlapIntersectingParentsAtDepth_iff {d : ℕ} {Q S T : TriadicCube d} {m : ℕ} : T ∈ overlapIntersectingParentsAtDepth Q S m ↔ T ∈ descendantsAtDepth Q m ∧ (overlapCubeSet S ∩ cubeSet T).Nonempty

theorem HCPolySupport.vecNormSq_cubeIncrementVec_le_overlapIntersectingParentEnergy_sum {d : ℕ} {Q S : TriadicCube d} {m : ℕ} (u : Vec d → Vec d) (hSsub : overlapCubeSet S ⊆ cubeSet Q) {x : Vec d} (hxS : x ∈ overlapCubeSet S) (huChild : ∀ T ∈ descendantsAtDepth Q m, ∀ R ∈ childCubes T, MeasureTheory.MemLp u 2 (normalizedCubeMeasure R)) : vecNormSq (cubeIncrementVec Q (m + 1) u x) ≤ ∑ T ∈ overlapIntersectingParentsAtDepth Q S m, ∑ R ∈ childCubes T, ∑ i : Fin d, cubeAverage R fun (y : Vec d) => (u y i - cubeAverageVec T u i) ^ 2

Pointwise local-neighbor version: on an overlap cube contained in Q, a martingale increment is paid by child energies of only those depth-m parents which meet that overlap cube.

theorem HCPolySupport.overlapCubeLpNorm_fluctuationIncrement_le_fourParentEnergySum {d : ℕ} {Q S : TriadicCube d} {m : ℕ} (u : Vec d → Vec d) (hSsub : overlapCubeSet S ⊆ cubeSet Q) (hinc : MeasureTheory.MemLp (cubeIncrementVec Q (m + 1) u) 2 (normalizedOverlapCubeMeasure S)) (huChild : ∀ T ∈ descendantsAtDepth Q m, ∀ R ∈ childCubes T, MeasureTheory.MemLp u 2 (normalizedCubeMeasure R)) : overlapCubeLpNorm S 2 (overlapCubeFluctuationVec S (cubeIncrementVec Q (m + 1) u)) ^ 2 ≤ 4 * ∑ T ∈ overlapIntersectingParentsAtDepth Q S m, ∑ R ∈ childCubes T, ∑ i : Fin d, cubeAverage R fun (y : Vec d) => (u y i - cubeAverageVec T u i) ^ 2

Overlap-fluctuation local-neighbor budget for one martingale increment.