High-contrast homogenization: Provider.Response.PreYoungPrimalProjectionGeometry #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
The primal cutoff oscillation is first estimated against finite-depth cube projections of the optimizer field. The projection expansion is reindexed by adapted nested cells, and its limit is identified with the physical pairing.
theorem
HCPolySupport.HighContrast.Response.sum_range_eq_sum_Ico_descending
(s : ℤ)
(N : ℕ)
(F : ℤ → ℝ)
:
theorem
HCPolySupport.HighContrast.Response.integrableOn_diagonalWeakState_fst_component_of_aligned
{d : ℕ}
{q : Mat d}
(hq : Matrix.PosDef q)
{k t : ℤ}
(hkt : k ≤ t)
{w : Fin d → ℤ}
(hw : w ∈ alignedIndex q k t)
(a : CoeffSpace d)
(p r : Vec d)
(i : Fin d)
:
MeasureTheory.IntegrableOn (fun (x : Vec d) => (diagonalWeakState hq t a p r x).1 i) (adaptedCellAt q k w)
MeasureTheory.volume
theorem
HCPolySupport.HighContrast.Response.integrableOn_vecDot_diagonalWeakState_pullback
{d : ℕ}
{q : Mat d}
(hq : Matrix.PosDef q)
{s t : ℤ}
(hst : s ≤ t)
{z : Fin d → ℤ}
(hz : z ∈ alignedIndex q s t)
(a : CoeffSpace d)
(p r Qcen : Vec d)
:
MeasureTheory.IntegrableOn (fun (y : Vec d) => vecDot Qcen (diagonalWeakState hq t a p r (matVecMul q y)).1)
(cubeSet (translateCube z (originCube d s))) MeasureTheory.volume
theorem
HCPolySupport.HighContrast.Response.integral_double_avsum_le_of_half_integral_row_bounds
{α : Type u_1}
{ι : Type u_2}
{κ : Type u_3}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
(Z : Finset ι)
(W : Finset κ)
(pair : ι → κ → α → ℝ)
(energy load : κ → ℝ)
(hint : ∀ z ∈ Z, ∀ w ∈ W, MeasureTheory.Integrable (pair z w) μ)
(hrow : ∀ w ∈ W, (avsum Z fun (z : ι) => 1 / 2 * ∫ (a : α), pair z w a ∂μ) ≤ energy w * load w)
:
theorem
HCPolySupport.HighContrast.Response.descendantsAtDepth_translated_root_eq_nested_labels
{d : ℕ}
{q : Mat d}
(hq : Matrix.PosDef q)
{k s : ℤ}
(hks : k ≤ s)
(z : Fin d → ℤ)
:
descendantsAtDepth (translateCube z (originCube d s)) (s - k).toNat = Finset.image (fun (w : Fin d → ℤ) => translateCube (nestedLabel k s z w) (originCube d k)) (alignedIndex q k s)
theorem
HCPolySupport.HighContrast.Response.cubeBesovCircDepthAverage_pullback_eq_nested_avsum
{d : ℕ}
{q : Mat d}
(hq : Matrix.PosDef q)
{k s : ℤ}
(hks : k ≤ s)
(z : Fin d → ℤ)
(g : Vec d → ℝ)
:
cubeBesovCircDepthAverage (translateCube z (originCube d s)) 1 (fun (y : Vec d) => g (matVecMul q y)) (s - k).toNat = avsum (alignedIndex q k s) fun (w : Fin d → ℤ) => |volumeAverage (adaptedCellAt q k (nestedLabel k s z w)) g|
theorem
HCPolySupport.HighContrast.Response.volumeAverage_vecDot_fst_eq_vecDot_blockCellAverage
{d : ℕ}
(U : Set (Vec d))
(F : Vec d → BlockVec d)
(Qcen : Vec d)
(hF : ∀ (i : Fin d), MeasureTheory.IntegrableOn (fun (x : Vec d) => (F x).1 i) U MeasureTheory.volume)
:
theorem
HCPolySupport.HighContrast.Response.cubeBesovCircDepthAverage_primal_eq_nested_cellPair_avsum
{d : ℕ}
{q : Mat d}
(hq : Matrix.PosDef q)
{k s : ℤ}
(hks : k ≤ s)
(z : Fin d → ℤ)
(F : Vec d → BlockVec d)
(Qcen : Vec d)
(hF :
∀ w ∈ alignedIndex q k s,
∀ (i : Fin d),
MeasureTheory.IntegrableOn (fun (x : Vec d) => (F x).1 i) (adaptedCellAt q k (nestedLabel k s z w))
MeasureTheory.volume)
:
cubeBesovCircDepthAverage (translateCube z (originCube d s)) 1 (fun (y : Vec d) => vecDot Qcen (F (matVecMul q y)).1)
(s - k).toNat = avsum (alignedIndex q k s) fun (w : Fin d → ℤ) =>
|vecDot Qcen (blockCellAverage (adaptedCellAt q k (nestedLabel k s z w)) F).1|
theorem
HCPolySupport.HighContrast.Response.abs_cubeBesovPairing_cubeProjection_le_depth_sum
{d : ℕ}
(Q : TriadicCube d)
(f G : Vec d → ℝ)
(N : ℕ)
(K : ℕ → ℝ)
(hGInt : MeasureTheory.IntegrableOn G (cubeSet Q) MeasureTheory.volume)
(hf : MeasureTheory.MemLp f 1 (normalizedCubeMeasure Q))
(hfTop : ∀ j < N, ∀ R ∈ descendantsAtDepth Q j, MeasureTheory.MemLp (cubeFluctuation R f) ⊤ (normalizedCubeMeasure R))
(hmean : cubeAverage Q f = 0)
(hres : ∀ j < N, ∀ x ∈ cubeSet Q, |cubeProjectionResidual Q j f x| ≤ K j)
:
|cubeBesovPairing Q f (cubeProjection Q N G)| ≤ ∑ j ∈ Finset.range N, K j * cubeBesovCircDepthAverage Q 1 G (j + 1)
theorem
HCPolySupport.HighContrast.Response.cutoff_projectionResidual_le_sharp
{d : ℕ}
[NeZero d]
{q : Mat d}
(hq : Matrix.PosDef q)
(s t : ℤ)
(z : Fin d → ℤ)
(j : ℕ)
{x : Vec d}
(hx : x ∈ cubeSet (translateCube z (originCube d s)))
:
have R := translateCube z (originCube d s);
have phi := fun (y : Vec d) => adaptedPreYoungCutoff q hq t (matVecMul q y);
have f := fun (y : Vec d) => phi y - cubeAverage R phi;
|cubeProjectionResidual R j f x| ≤ 32 * ↑d ^ 2 * smoothTransitionProfile.derivBound * 3 ^ (-(t - s + ↑j))
theorem
HCPolySupport.HighContrast.Response.abs_cutoff_projected_primal_pairing_le_depth_sum
{d : ℕ}
[NeZero d]
{q : Mat d}
(hq : Matrix.PosDef q)
(s t : ℤ)
(z : Fin d → ℤ)
(F : Vec d → BlockVec d)
(Qcen : Vec d)
(N : ℕ)
(hGInt :
MeasureTheory.IntegrableOn (fun (y : Vec d) => vecDot Qcen (F (matVecMul q y)).1)
(cubeSet (translateCube z (originCube d s))) MeasureTheory.volume)
:
have R := translateCube z (originCube d s);
have phi := fun (y : Vec d) => adaptedPreYoungCutoff q hq t (matVecMul q y);
have f := fun (y : Vec d) => phi y - cubeAverage R phi;
have G := fun (y : Vec d) => vecDot Qcen (F (matVecMul q y)).1;
|cubeBesovPairing R f (cubeProjection R N G)| ≤ ∑ j ∈ Finset.range N,
32 * ↑d ^ 2 * smoothTransitionProfile.derivBound * 3 ^ (-(t - s + ↑j)) * cubeBesovCircDepthAverage R 1 G (j + 1)
theorem
HCPolySupport.HighContrast.Response.abs_cutoff_projected_primal_pairing_le_nested_depth_sum
{d : ℕ}
[NeZero d]
{q : Mat d}
(hq : Matrix.PosDef q)
(s t : ℤ)
(z : Fin d → ℤ)
(F : Vec d → BlockVec d)
(Qcen : Vec d)
(N : ℕ)
(hGInt :
MeasureTheory.IntegrableOn (fun (y : Vec d) => vecDot Qcen (F (matVecMul q y)).1)
(cubeSet (translateCube z (originCube d s))) MeasureTheory.volume)
(hF :
∀ j < N,
∀ w ∈ alignedIndex q (s - ↑(j + 1)) s,
∀ (i : Fin d),
MeasureTheory.IntegrableOn (fun (x : Vec d) => (F x).1 i)
(adaptedCellAt q (s - ↑(j + 1)) (nestedLabel (s - ↑(j + 1)) s z w)) MeasureTheory.volume)
:
have R := translateCube z (originCube d s);
have phi := fun (y : Vec d) => adaptedPreYoungCutoff q hq t (matVecMul q y);
have f := fun (y : Vec d) => phi y - cubeAverage R phi;
have G := fun (y : Vec d) => vecDot Qcen (F (matVecMul q y)).1;
|cubeBesovPairing R f (cubeProjection R N G)| ≤ ∑ j ∈ Finset.range N,
32 * ↑d ^ 2 * smoothTransitionProfile.derivBound * 3 ^ (-(t - s + ↑j)) * avsum (alignedIndex q (s - ↑(j + 1)) s) fun (w : Fin d → ℤ) =>
|vecDot Qcen (blockCellAverage (adaptedCellAt q (s - ↑(j + 1)) (nestedLabel (s - ↑(j + 1)) s z w)) F).1|
theorem
HCPolySupport.HighContrast.Response.abs_cutoff_projected_primal_pairing_subSkew_le_nested_depth_sum
{d : ℕ}
[NeZero d]
{q : Mat d}
(hq : Matrix.PosDef q)
{s t : ℤ}
(hst : s ≤ t)
{z : Fin d → ℤ}
(hz : z ∈ alignedIndex q s t)
(g : Mat d)
(hg : IsSkewMat g)
(a : CoeffSpace d)
(p r Qcen : Vec d)
(N : ℕ)
:
have R := translateCube z (originCube d s);
have phi := fun (y : Vec d) => adaptedPreYoungCutoff q hq t (matVecMul q y);
have f := fun (y : Vec d) => phi y - cubeAverage R phi;
have F := diagonalWeakState hq t (a.subSkew g hg) p r;
have G := fun (y : Vec d) => vecDot Qcen (F (matVecMul q y)).1;
|cubeBesovPairing R f (cubeProjection R N G)| ≤ ∑ j ∈ Finset.range N,
32 * ↑d ^ 2 * smoothTransitionProfile.derivBound * 3 ^ (-(t - s + ↑j)) * avsum (alignedIndex q (s - ↑(j + 1)) s) fun (w : Fin d → ℤ) =>
|vecDot Qcen (blockCellAverage (adaptedCellAt q (s - ↑(j + 1)) (nestedLabel (s - ↑(j + 1)) s z w)) F).1|
noncomputable def
HCPolySupport.HighContrast.Response.primalProjectedOscillation
{d : ℕ}
{q : Mat d}
(hq : Matrix.PosDef q)
(s t : ℤ)
(g : Mat d)
(hg : IsSkewMat g)
(p r Qcen : Vec d)
(N : ℕ)
(a : CoeffSpace d)
:
The aligned-cell average of the centered cutoff paired with the depth-N
projection of the primal state component in direction Qcen, after skew subtraction.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
HCPolySupport.HighContrast.Response.primalPhysicalOscillation
{d : ℕ}
{q : Mat d}
(hq : Matrix.PosDef q)
(s t : ℤ)
(g : Mat d)
(hg : IsSkewMat g)
(p r Qcen : Vec d)
(a : CoeffSpace d)
:
The aligned-cell average of the centered cutoff paired with the full
primal state component in direction Qcen, after skew subtraction.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
HCPolySupport.HighContrast.Response.abs_primal_projected_oscillation_le_nested_depth_sum
{d : ℕ}
[NeZero d]
{q : Mat d}
(hq : Matrix.PosDef q)
{s t : ℤ}
(hst : s ≤ t)
(g : Mat d)
(hg : IsSkewMat g)
(p r Qcen : Vec d)
(N : ℕ)
(a : CoeffSpace d)
:
|primalProjectedOscillation hq s t g hg p r Qcen N a| ≤ ∑ j ∈ Finset.range N,
32 * ↑d ^ 2 * smoothTransitionProfile.derivBound * 3 ^ (-(t - s + ↑j)) * avsum (alignedIndex q s t) fun (z : Fin d → ℤ) =>
avsum (alignedIndex q (s - ↑(j + 1)) s) fun (w : Fin d → ℤ) =>
|vecDot Qcen
(blockCellAverage (adaptedCellAt q (s - ↑(j + 1)) (nestedLabel (s - ↑(j + 1)) s z w))
(diagonalWeakState hq t (a.subSkew g hg) p r)).1|
theorem
HCPolySupport.HighContrast.Response.primal_cutoff_oscillation_eq_unprojected_pairing
{d : ℕ}
{q : Mat d}
(hq : Matrix.PosDef q)
(s t : ℤ)
(w : Fin d → ℤ)
(F : Vec d → BlockVec d)
(Qcen : Vec d)
:
have R := translateCube w (originCube d s);
have phi := fun (y : Vec d) => adaptedPreYoungCutoff q hq t (matVecMul q y);
have f := fun (y : Vec d) => phi y - cubeAverage R phi;
have G := fun (y : Vec d) => vecDot Qcen (F (matVecMul q y)).1;
(volumeAverage (adaptedCellAt q s w) fun (x : Vec d) =>
(adaptedPreYoungCutoff q hq t x - volumeAverage (adaptedCellAt q s w) (adaptedPreYoungCutoff q hq t)) * vecDot Qcen (F x).1) = cubeBesovPairing R f G
theorem
HCPolySupport.HighContrast.Response.projected_primal_pairing_tendsto_physical
{d : ℕ}
(Q : TriadicCube d)
(f G : Vec d → ℝ)
(C : ℝ)
(hGInt : MeasureTheory.IntegrableOn G (cubeSet Q) MeasureTheory.volume)
(hfInt : MeasureTheory.IntegrableOn f (cubeSet Q) MeasureTheory.volume)
(hC : 0 ≤ C)
(hfBound : ∀ x ∈ cubeSet Q, |f x| ≤ C)
:
Filter.Tendsto (fun (n : ℕ) => cubeBesovPairing Q f (cubeProjection Q (n + 1) G)) Filter.atTop
(nhds (cubeBesovPairing Q f G))