NearGraph.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The near part of the independent angular energy

Nearness is imposed on both actual center displacements. Integer grid packing gives a dimensional degree bound; positive Schur integration then controls this part by the sum of the original child energies. No angular localization or separation of the two parent cells is used.

theorem OAI.Falconer.DyadicCube.neighbor_card line 18
def OAI.Falconer.nearDyadicEdge line 37
theorem OAI.Falconer.nearDyadicEdge_symm line 42
theorem OAI.Falconer.nearDyadic_degree line 47

theorem OAI.Falconer.dyadic_near_energy_bound line 70

Source documentation

The near contribution after exact model-mass splitting. This is the analytic near reduction before the profile normalization.

theorem dyadic_near_energy_bound {d n L : ℕ} (Q₁ Q₂ : DyadicCube d)
    (hQ₁ : 0 < Q₁.side) (hQ₂ : 0 < Q₂.side)
    (μ ν : Measure (Space d)) [IsFiniteMeasure μ] [IsFiniteMeasure ν]
    (M₁ M₂ : ℝ) (hM₁ : 0 < M₁) (hM₂ : 0 < M₂)
    (b c : Space d → Sphere d → ℂ)
    (hb : Measurable (Function.uncurry b)) (hc : Measurable (Function.uncurry c))
    {B C : ℝ} (hB : 0 ≤ B) (hC : 0 ≤ C)
    (hbB : ∀ x w, ‖b x w‖ ≤ B) (hcC : ∀ x w, ‖c x w‖ ≤ C)
    {τ : ℝ} (hL₁ : τ*((2:ℝ)^n/Q₁.side) ≤ L)
    (hL₂ : τ*((2:ℝ)^n/Q₂.side) ≤ L)
    (a p v : ℝ) (Ψ : ℝ → ℝ)
    [IsFiniteMeasure (PlanarFalconer.sourceAngularShellMeasure v Ψ)] :
…

Mentions: OAI.Falconer.DyadicCube, OAI.Falconer.Space, OAI.Falconer.Sphere, OAI.PlanarFalconer.sourceAngularShellMeasure