Genuine endpoints of a finite halfspace slice

The scalar boundary bookkeeping for the cell divergence theorem: a finite endpoint is either an artificial outer endpoint, where the compact field vanishes, or the unique genuine facet having the appropriate orientation.

noncomputable def LiebThirring.halfspaceFaceValue {ι : Type u_1} (a b : ι → ℝ) (g : ℝ → ℝ) (i : ι) : ℝ

The value of a scalar field at a genuine transverse constraint endpoint.

Equations

• LiebThirring.halfspaceFaceValue a b g i = if ∀ (j : ι), j ≠ i → b i / a i * a j < b j then g (b i / a i) else 0

theorem LiebThirring.sum_positive_halfspaceFaceValue {ι : Type u_1} [Fintype ι] (a b : ι → ℝ) (g : ℝ → ℝ) (U B : ℝ) (hmin : ∀ (i : ι), 0 < a i → U ≤ b i / a i) (hclosed : ∀ (i : ι), U * a i ≤ b i) (hregular : ∀ (i j : ι), i ≠ j → U * a i = b i → U * a j = b j → False) (hupper : U = B ∨ ∃ (i : ι), 0 < a i ∧ U = b i / a i) (hzero : ∀ (t : ℝ), B ≤ t → g t = 0) : (∑ i : ι, if 0 < a i then halfspaceFaceValue a b g i else 0) = g U

Positive-oriented genuine facets give precisely the value at the upper end.

theorem LiebThirring.halfspaceFaceValue_reflect {ι : Type u_1} (a b : ι → ℝ) (g : ℝ → ℝ) (i : ι) : halfspaceFaceValue (fun (i : ι) => -a i) b (fun (t : ℝ) => g (-t)) i = halfspaceFaceValue a b g i

theorem LiebThirring.sum_negative_halfspaceFaceValue {ι : Type u_1} [Fintype ι] (a b : ι → ℝ) (g : ℝ → ℝ) (L A : ℝ) (hmax : ∀ (i : ι), a i < 0 → b i / a i ≤ L) (hclosed : ∀ (i : ι), L * a i ≤ b i) (hregular : ∀ (i j : ι), i ≠ j → L * a i = b i → L * a j = b j → False) (hlower : L = A ∨ ∃ (i : ι), a i < 0 ∧ L = b i / a i) (hzero : ∀ t ≤ A, g t = 0) : (∑ i : ι, if a i < 0 then halfspaceFaceValue a b g i else 0) = g L

Negative-oriented genuine facets give precisely the value at the lower end.