OAI.ScalarConductivity.main_nonuniqueness
ProvedThe theorem states that the defined proposition MainStatement holds, namely that scalar conductivity is not determined by its Dirichlet-to-Neumann operator on the ball of radius 3 in ℝ³. Here H¹ is the closure, in L² of the ball (Lebesgue measure restricted to the open ball of radius 3) with values in ℝ⁴, of the jets (f, ∇f) of smooth functions f on ℝ³ with square-integrable jets, and H¹₀ is the part of H¹ lying in the closure of jets of smooth compactly supported functions whose support lies in the ball. The trace space is the quotient H¹/H¹₀, and a Dirichlet-to-Neumann operator is a continuous linear map from the trace space to its continuous dual. For a conductivity γ, the energy form is E_γ(u,v)=∫ γ ∇u·∇v over the ball, and u is γ-harmonic if E_γ(u,h)=0 for every h in H¹₀. A map Λ is a Dirichlet-to-Neumann operator for γ if, for each trace f, there is a unique γ-harmonic u in H¹ with trace f, and Λ f applied to the trace of any v in H¹ equals E_γ(u,v). The claim is that there exist two functions γ₀, γ₁ on ℝ³, constants 0<c<C, and a single operator Λ such that both γ₀ and γ₁ are measurable and essentially bounded on the ball, satisfy c ≤ γᵢ ≤ C almost everywhere on the ball, and equal 1 almost everywhere on the region r<|x|<3 for some radius r with 0<r<3 (possibly different for each), the set where γ₀ ≠ γ₁ has positive measure, and Λ is a Dirichlet-to-Neumann operator for both γ₀ and γ₁.
-- Generated from openai/math @ adc7f1241b42e322a6451854ab7e4b4c146bf78a -- Source: lean/ComparatorChallenges/Conductivity.lean; bytes 2793..2849 -- Kind: theorem; original declaration names and bodies preserved. -- Source groups are independent. Target: Lean 4.33.1; see compilation.json. import Mathlib import Definitions.Def_Conductivity namespace OAI noncomputable section open MeasureTheory open scoped ENNReal namespace ScalarConductivity
theorem main_nonuniqueness : MainStatement := by sorry end ScalarConductivity end end OAI
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.